local_bound
plain-language theorem explainer
On each cardinality slice the nonlinear Regge action admits a cubic Taylor remainder about the zero potential, controlled by the slice's local constant times the cube of the potential norm, inside a positive local radius on the canonical periodic Freudenthal torus. Analysts closing the D2 residual-vanishing target cite this bound. The proof is a one-line unpack of the slice's built-in local-correspondence witness.
Claim. Let $S$ be a canonical periodic six-tet volume quadrature slice. Write $T_S$ for its canonical encoded periodic Freudenthal torus, $R$ for the Regge action on $T_S$, and $ES$ for the periodic edge-stencil Dirichlet action. There exist $r_S>0$ and $C_S\ge 0$ (the local radius and local constant of $S$) such that for every vertex potential $\xi$ on $T_S$, if $\|\xi\|<r_S$ then $\|R(\xi)-R(0)-\tfrac12 ES(\xi)\|\le C_S\|\xi\|^3$.
background
The D2 product-filter program compares the full nonlinear Regge action on a family of periodic tetrahedral meshes to a continuum integral. Each cardinality slice already carries a Track 1.B local-correspondence witness: a positive radius and a nonnegative constant such that the cubic Taylor bound
$|R(\xi)-R(0)-\tfrac12 ES(\xi)|\le C|\xi|^3$
holds for all vertex potentials inside that radius. Here $R$ is the concrete Regge action on the canonical encoded periodic Freudenthal torus attached to the slice, and $ES$ is the quadratic periodic edge-stencil Dirichlet form that is the continuum Hessian at the zero potential.
The module's job is to discharge the residual-vanishing target that earlier D2 data treated as a supplied analytic field. The only primitive input needed is this local cubic bound; a per-slice damping schedule then keeps every scaled probe inside the radius and drives the residual coefficient below a universal envelope. The present declaration simply re-states the cubic bound in the form used by the damping construction.
proof idea
One-line wrapper. The slice structure already packages the local-correspondence data as an existential field hLocal. After installing the three NeZero instances for the lattice dimensions, the proof is exact on the second conjunct of the second choose_spec of that witness, which is precisely the cubic inequality for every potential inside the local radius.
why it matters
This is the primitive curvature bound that the whole D2 damped-schedule closure rests on. Downstream, normalized_regge_sub_limit_abs_le divides the same remainder by $s^2$ to control the normalized nonlinear Regge action minus the quadratic Dirichlet limit for scaled probes. That normalized form, together with the damping factor built from the local radius, local constant, probe-norm sums, and limiting cell volume, forces the two-scale residual to vanish uniformly on the product filter with no supplied analytic field.
In the Recognition Gravity stack this closes D2 open item 2 of the scoping audit: residual vanishing is derived, not hypothesized. The full nonlinear Regge-to-continuum product-filter convergence for the damped family then needs only the quadrature limit. The declaration sits entirely on the discrete geometric side; it does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law, but it is the analytic hinge that lets those continuum limits attach to the discrete Regge data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.