normalized_regge_sub_limit_abs_le
plain-language theorem explainer
On each periodic tet-six-tet quadrature slice, the nonlinear Regge action of a scaled probe, normalized by s², differs from half the quadratic Dirichlet energy by at most the slice cubic constant times |s| times the cubed probe norm, whenever the scaled probe lies inside the local-correspondence ball. Gravity analysts cite it when converting the Track 1.B cubic Taylor bound into a two-scale residual estimate. The proof divides the local cubic bound by s² and uses quadratic homogeneity of the Dirichlet energy.
Claim. Let $S$ be a canonical periodic tet-six-tet volume quadrature slice and let $s\neq 0$. For every vertex potential $\xi$ on the encoded periodic Freudenthal torus of $S$, if $\|s\cdot\xi\|<r_S$ (the slice local-correspondence radius), then $$\Bigl|\frac{R(s\cdot\xi)}{s^2}-\tfrac12\,ES(\xi)\Bigr|\le C_S\,|s|\,\|\xi\|^3,$$ where $R$ is the Regge action, $ES$ is the canonical Dirichlet energy, and $C_S$ is the slice cubic constant.
background
The module closes D2 open item 2 from the scoping audit: the uniform residual of full nonlinear Regge minus quadrature must be derived, not supplied as a hypothesis field. Every cardinality slice already carries Track 1.B local correspondence: a radius $r_S$ and cubic constant $C_S$ such that $|R(\xi)-R(0)-\tfrac12 ES(\xi)|\le C_S|\xi|^3$ whenever $|\xi|<r_S$.
Here $R$ is the Regge action on the canonical encoded periodic Freudenthal torus of the slice, and $ES$ is the canonical Dirichlet energy (equivalently the periodic edge-stencil Dirichlet action). The zero potential has vanishing Regge action on the flat configuration. Dirichlet energy is homogeneous of degree two under real scaling of the probe.
The local radius and local constant are slice data extracted from that correspondence witness. The present statement is exactly the local cubic Taylor bound after dividing through by $s^2$, which is the normalization needed for two-scale residual estimates along a damped within-slice schedule.
proof idea
Apply the slice local cubic bound to the scaled probe $s\cdot\xi$ (hypothesis $|s\cdot\xi|<r_S$). Rewrite using three facts: Regge action of the zero potential vanishes on the flat configuration; canonical Dirichlet energy equals the periodic edge-stencil action; and canonicalDirichletEnergy_smul gives $ES(s\cdot\xi)=s^2 ES(\xi)$.
Algebraically rearrange so the normalized difference equals the un-normalized cubic remainder divided by $s^2$. Since $s^2>0$, absolute values pass through the quotient. Expand $|s\cdot\xi|^3=|s|^3|\xi|^3$ and factor $|s|^3=|s|,s^2$, cancel one $s^2$, and obtain the claimed cubic bound with coefficient $C_S|s||\xi|^3$.
why it matters
This lemma is the bridge from the primitive local-correspondence cubic bound to the damped-schedule residual control. Its sole downstream consumer is dampedSlice_residual_abs_le, which bounds the full nonlinear Regge aggregate minus the quadrature proxy by $|\sigma t|$ uniformly in the slice once the within-slice spacing is damped by the factor built from $r_S$, $C_S$, probe norms, and limiting cell volume.
That residual bound is what discharges D2 residual-vanishing without a supplied analytic field, so the product-filter residual target holds for the damped family. Combined with quadrature convergence, one obtains full nonlinear Regge to continuum product-filter convergence for damped families. In the broader RS gravity stack this is pure continuum discrete-geometry analysis (Regge calculus on Freudenthal triangulations), not a forcing-chain step, but it is required scaffolding closure for the D2 gravity audit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.