normalized_regge_sub_half_quadratic_abs_le
plain-language theorem explainer
Given a homogeneous quadratic Q and a cubic residual bound between the Regge action and half of Q near zero, the normalized residual after scaling a potential by s and dividing by s² is at most C|s|‖ξ‖³. Gravity Track 1.B cites this as the exact per-tetrahedron bound the damped-schedule D2 closure consumes. The proof is a short algebraic reduction: apply the cubic bound at s•ξ, use 2-homogeneity of Q, and rearrange the absolute value of a quotient.
Claim. Let $K$ be an incidence-consistent 3D triangulation and $Q$ a real functional on vertex potentials that is homogeneous of degree two. Suppose the Regge action vanishes at the zero potential, and that near zero it admits a cubic residual bound against $\tfrac12 Q$: for $\|\xi\|<r$, $\bigl\|\mathrm{Regge}(\xi)-\tfrac12 Q(\xi)\bigr\|\le C\|\xi\|^3$. Then for every $s\ne 0$ and every $\xi$ with $\|s\cdot\xi\|<r$, $\bigl|\mathrm{Regge}(s\cdot\xi)/s^2-\tfrac12 Q(\xi)\bigr|\le C|s|\|\xi\|^3$.
background
Track 1.B aims at a local correspondence between the nonlinear Regge action on a 3D triangulation and a quadratic stencil built from hinge deficits. Session 202 showed the legacy mixed-hinge identification was wrong-weighted against the seven-class edge stencil; the corrected endpoint takes the quadratic to be the canonical periodic mixed axis stencil.
The local correspondence asserts a cubic-Taylor residual: near the zero potential, Regge minus half the candidate quadratic is $O(|\xi|^3)$. The damped-schedule D2 closure does not consume that raw form. It needs a normalized residual after scaling the potential by a nonzero scalar $s$ and dividing the action by $s^2$, so the quadratic term becomes scale-invariant and the cubic remainder carries an explicit factor $|s|$.
This lemma isolates that normalization for an arbitrary 2-homogeneous $Q$ already satisfying the cubic bound and vanishing of Regge at zero. No special structure of the axis stencil is used here; that specialization is deferred to the downstream axis instance.
proof idea
Instantiate the cubic residual hypothesis at the scaled potential $s\cdot\xi$ (which is inside the ball by assumption). Rewrite using vanishing of Regge at zero and 2-homogeneity of $Q$, so the quadratic term becomes $\tfrac12 s^2 Q(\xi)$. Convert the vector-norm residual into an absolute value.
Algebraically identify the target normalized difference with the residual divided by $s^2$ (field simplification; $s^2>0$ by positivity). Pass the absolute value through the quotient. Expand $|s\cdot\xi|^3=|s|^3|\xi|^3$ and rewrite $|s|^3=|s|,s^2$. Congruence of the inequality under division by the positive $s^2$, then cancel, yields the claimed bound $C|s||\xi|^3$.
why it matters
This is the parametric D2 hook of the corrected Track 1.B module. Its sole consumer is axis_normalized_regge_bound_of_correspondence, which specializes $Q$ to the canonical periodic mixed axis stencil under the corrected local correspondence and produces the existential $(r,C)$ package the damped-schedule closure expects.
As the module doc states, the bound is proved for arbitrary homogeneous $Q$, so "the whole damped pipeline transfers to the corrected quadratic the day the corrected gate closes." The corrected gate itself remains named OPEN; this lemma does not close it. It only ensures that once the axis correspondence is available as a hypothesis, the normalized residual bound needed by D2 damping is free.
In the broader gravity track this sits downstream of the rigidity result that at most one homogeneous quadratic can satisfy the local correspondence, and of the Session 202 mismatch that selects the axis stencil over the legacy edge stencil.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.