axis_normalized_regge_bound_of_correspondence
plain-language theorem explainer
Under the corrected axis-stencil local correspondence on a periodic Freudenthal torus, the scale-normalized nonlinear Regge action converges to half the axis-stencil quadratic with a cubic residual bound. Gravity workers on the Track 1.B damped D2 pipeline cite this as the constructive damping hook. The proof unpacks the correspondence witness and feeds it to the parametric normalized residual lemma with axis homogeneity and flat vanishing.
Claim. Let $N_x,N_y,N_z>2$. Suppose the corrected Track 1.B local correspondence holds on the canonical periodic Freudenthal torus of those sizes: the nonlinear Regge action is cubic-Taylor equivalent to the mixed axis-stencil quadratic $Q_{\mathrm{axis}}$. Then there exist $r>0$ and $C\ge 0$ such that for every $s\neq 0$ and every vertex potential $\xi$, if $\|s\cdot\xi\|<r$, then $\bigl|\mathrm{Regge}(s\cdot\xi)/s^2 - \tfrac12 Q_{\mathrm{axis}}(\xi)\bigr| \le C\,|s|\,\|\xi\|^3$.
background
Track 1.B links the discrete Regge action on a periodic Freudenthal triangulation to a local quadratic cost. Session 202 showed the legacy seven-class edge stencil is wrong-weighted at the $N=5$ single-vertex bump; the mixed hinge-deficit quadratic matches the rational axis stencil instead. This module supplies the corrected endpoint: local cubic-Taylor correspondence with that axis stencil as $Q$.
The hypothesis CanonicalPeriodicAxisStencilLocalCorrespondence is exactly ReggeLocalQuadraticCorrespondence at $Q=$ the mixed axis-stencil action on the canonical encoded periodic Freudenthal torus (grid sizes $>2$). The correspondence asserts a neighborhood radius and constant controlling the cubic remainder between the nonlinear Regge functional and $\tfrac12 Q$.
The sibling lemma normalized_regge_sub_half_quadratic_abs_le packages the per-tetrahedron normalized residual bound parametrically in any homogeneous quadratic $Q$ that vanishes at the flat (zero) potential. That bound is the constructive input the damped D2 schedule closure consumes.
proof idea
Term-mode unpack-and-apply. Destructure the axis correspondence into radius $r$, constant $C$, positivity, and the raw residual witness. Reassemble the same $r,C$ and, for each scale $s\neq 0$ and potential $\xi$ in the small ball, invoke the parametric normalized residual lemma on:
- the torus complex and its flatness hypothesis,
- the mixed axis-stencil action as $Q$,
- exact $a^2$-homogeneity of that stencil under scalar multiplication of potentials,
- vanishing of the periodic Regge action at the canonical flat (zero) configuration. The residual witness from the correspondence is passed through unchanged; no new estimates are proved here.
why it matters
This is the D2 hook named in the module: the corrected endpoint feeds the damped-schedule closure. After the Session 202 finite audit forced the axis stencil over the legacy edge stencil, the pipeline still needed the normalized residual bound at that corrected $Q$. The present theorem is the axis instance of the parametric residual lemma, so the same constructive damping constants used by damped D2 apply under the corrected correspondence.
It sits downstream of the rigidity package in this module (uniqueness of homogeneous quadratics satisfying the correspondence; joint impossibility of both legacy and axis endpoints given the mismatch witness). The corrected gate at certificate scale $N=5$ remains named OPEN in the module; this bound is the analytic half of that gate once second-order Schläfli stationarity is already a theorem. No further used_by edges are recorded yet; the intended consumer is the damped D2 closure path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.