localConstant
plain-language theorem explainer
Extracts the cubic Taylor constant C_S from a cardinality slice's Track 1.B local-correspondence witness. Gravity and discrete-Regge analysts cite it when bounding nonlinear residual terms on Freudenthal tori. The body is a pure projection: NeZero instances for the lattice sizes, then choose on the existential package in hLocal.
Claim. For a canonical periodic six-tet volume quadrature slice $S$ along a filter, $\mathrm{localConstant}(S)\in\mathbb{R}$ is the cubic constant $C_S$ from the local-correspondence witness of $S$: there exist $r_S>0$ and $C_S$ such that $\|R(\xi)-R(0)-\tfrac12 ES(\xi)\|\le C_S\|\xi\|^3$ whenever $\|\xi\|<r_S$.
background
Module D2DampedScheduleClosure closes D2 open item 2 from the scoping audit: the uniform residual vanishing target is derived from the primitive curvature bound rather than supplied as an analytic hypothesis field. 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 pair $(r_S,C_S)$ is packaged existentially on the slice. The companion extractor localRadius yields $r_S$; this definition yields $C_S$. Downstream residual bookkeeping multiplies $C_S$ by limiting cell volume and cubed probe-norm sums to form the per-slice residual coefficient used in the damped schedule.
proof idea
Definition, not a proof. Install NeZero instances for the three lattice cardinalities from the slice, then project the second component of the chosen witness of S.hLocal via choose_spec.choose. No algebraic rewriting; pure existential unpacking of the local-correspondence package.
why it matters
Supplies the cubic constant $C_S$ that every residual estimate in this module multiplies against. Feeds local_bound (the cubic Taylor bound restated on the encoded periodic Freudenthal torus), localConstant_nonneg, normalized_regge_sub_limit_abs_le (normalized nonlinear Regge minus Dirichlet limit $\le C_S|s||\xi|^3$), and residualCoefficient ($|V_S|/6\cdot C_S\cdot\sum|\xi_\tau|^3$). That coefficient enters the damping factor $d_S$ and the uniform bound in dampedSlice_residual_abs_le, which is the engine discharging D2 residual vanishing for damped families without a supplied analytic field. Landmark link: discrete curvature control on the eight-tick / three-dimensional lattice scaffolding underlying ILG gravity, not a new continuum axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.