residualCoefficient
plain-language theorem explainer
Defines the per-slice residual coefficient K_S as the product of absolute limiting cell volume over six, the local cubic Taylor constant, and the sum of cubed probe norms. Gravity analysts cite it when building the damped within-slice schedule that forces the nonlinear Regge residual to vanish. The body is a direct arithmetic combination of three already-defined slice quantities.
Claim. For a canonical periodic six-tet volume quadrature slice $S$, the residual coefficient is $K_S = \frac{|V_S|}{6}\, C_S \, \sum_\tau \|\xi_\tau\|^3$, where $V_S$ is the limiting cell volume, $C_S$ is the local-correspondence cubic constant, and the sum runs over the slice tetrahedra probe norms.
background
The module closes D2 open item 2 from the scoping audit: the uniform residual-vanishing target on a product filter. Previously that target was a supplied analytic field; here it is derived from the Track 1.B local correspondence alone. Each cardinality slice carries a cubic Taylor bound $|R(\xi)-R(0)-\tfrac12 ES(\xi)| \le C|\xi|^3$ for $|\xi|<r$.
The residual coefficient packages the three slice-local ingredients that control the size of the full nonlinear Regge-minus-quadrature residual after within-slice refinement: the absolute limiting cell volume $|V_S|$ (weighted by $1/6$), the cubic constant $C_S$ extracted as localConstant, and the sum of cubed probe norms probeCubeSum. Module text writes this package as $K_S = (|V_S|/6)\cdot C_S\cdot\sum_\tau|\xi_\tau|^3$.
Together with the local radius $r_S$ and the plain probe-norm sum, $K_S$ determines the per-slice damping factor that keeps every scaled probe inside the correspondence ball and shrinks the residual below a universal envelope.
proof idea
Pure definition, not a proof. After installing the three NeZero instances for the slice grid dimensions, the body multiplies three real quantities already defined on the same slice type: absolute value of S.data.limitCellVolume divided by six, localConstant S, and probeCubeSum S. No lemmas are applied.
why it matters
This coefficient is the second half of the damping factor $d_S = \min\bigl(r_S/(1+\sum|\xi_\tau|),, 1/(1+K_S)\bigr)$. Downstream, dampingFactor uses it directly; residualCoefficient_nonneg and one_add_residualCoefficient_pos guarantee the second min-branch is well-defined and positive; dampingFactor_mul_residualCoefficient_le_one shows the product is at most one.
Those facts feed dampedSlice_residual_abs_le, which bounds the damped slice residual by $|\sigma(t)|$ uniformly in the slice. That bound is the engine of dampedFamily_uniformResidual, discharging D2 residual-vanishing without a supplied analytic hypothesis and leaving only quadrature convergence for the full Regge-to-continuum product-filter theorem. In the gravity track this is the concrete arithmetic object that turns a local cubic curvature bound into a schedule-controlled residual.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.