localConstant_nonneg
plain-language theorem explainer
The local cubic Taylor constant on a canonical periodic tet/six-tet volume quadrature slice is nonnegative. Residual and damped-schedule estimates in the D2 gravity closure cite this when assembling the per-slice residual coefficient from Track 1.B local correspondence. The proof is a short term extraction of the nonnegativity conjunct from the slice's packed local-correspondence witness.
Claim. Let $\ell$ be a filter on a type $\alpha$, and let $S$ be a canonical periodic tet/six-tet volume quadrature slice along $\ell$. Write $C_S$ for the local cubic Taylor constant carried by $S$ (the constant in the bound $\|R(\xi)-R(0)-\tfrac12 ES(\xi)\|\le C_S\|\xi\|^3$ for $\|\xi\|<r_S$). Then $0\le C_S$.
background
The module closes D2 open item 2 from the scoping audit: the uniform residual target for full nonlinear Regge minus quadrature, previously a supplied analytic field on the product-filter datum. Every cardinality slice already carries Track 1.B local correspondence (hLocal), the cubic Taylor bound
$|R(\xi)-R(0)-\tfrac12\cdot ES(\xi)|\le C\cdot|\xi|^3$ for $|\xi|<r$.
The slice packages witnesses $(r_S,C_S)$ for that bound. Sibling definitions name them localRadius and localConstant. The damped within-slice schedule uses
$d_S=\min\bigl(r_S/(1+\sum_\tau|\xi_\tau|),,1/(1+K_S)\bigr)$
with residual mass $K_S=(|V_S|/6)\cdot C_S\cdot\sum_\tau|\xi_\tau|^3$. Nonnegativity of $C_S$ is the first arithmetic fact needed before $K_S$ and the residual coefficient can be treated as nonnegative scalars in the damping argument.
proof idea
Term-mode projection, not a calculation. The slice type already records NeZero instances on the three grid cardinalities $N_x,N_y,N_z$; the proof reinstalls those instances so the local-correspondence field typechecks. It then opens the existential packed in hLocal (radius, constant, and the bound) and returns the nonnegativity conjunct on the constant. No external lemma is applied beyond that structure projection.
why it matters
Parent use is residualCoefficient_nonneg in the same module, which multiplies $|V_S|/6$, $C_S$, and the probe-cube sum and needs each factor nonnegative. That residual coefficient is the scalar the damped schedule drives below a slice-independent envelope $|\sigma(t)|$, so that dampedFamily_uniformResidual holds with no supplied analytic residual field.
In the Recognition gravity stack this is a small but load-bearing positivity lemma on the path from Track 1.B local curvature correspondence to product-filter continuum convergence of the full nonlinear Regge action. It does not touch the forcing chain (T5–T8) or the RCL directly; it sits inside the D2 analytic closure that turns a hypothesis-shaped residual target into a derived theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.