both_correspondences_force_equal_quadratics
plain-language theorem explainer
If both the legacy seven-class edge-stencil correspondence and the corrected axis-stencil correspondence hold on the same periodic Freudenthal torus, then the two quadratic forms agree at every vertex potential. Gravity theorists tracking the Track 1.B Regge/J-cost endpoint cite this rigidity step. The proof is a direct application of uniqueness for homogeneous quadratics satisfying the local cubic-Taylor correspondence.
Claim. Let $N_x,N_y,N_z\ge 3$. Write $P$ for the canonical encoded periodic Freudenthal torus of those sizes, and let $K$ be its triangulation. Suppose both the legacy local correspondence (with quadratic equal to the periodic edge-stencil Dirichlet action on $P$) and the corrected local correspondence (with quadratic equal to the canonical periodic mixed axis-stencil action) hold. Then for every vertex conformal potential $\xi:K^{(0)}\to\mathbb{R}$, the two actions agree: $\mathrm{EdgeStencil}(P,\xi)=\mathrm{AxisStencil}(N_x,N_y,N_z,\xi)$.
background
Track 1.B factors the local Regge/J-cost correspondence through a mixed hinge-deficit quadratic on a finite 3D triangulation. A vertex conformal potential is a real assignment to the vertices of the triangulation. The legacy endpoint takes the quadratic to be the seven-class periodic edge-stencil Dirichlet action; the corrected endpoint takes it to be the rational axis stencil that the Session 202 finite audit identifies with the mixed hinge-deficit quadratic.
ReggeLocalQuadraticCorrespondence packages the cubic-Taylor match between the Regge action and an arbitrary candidate quadratic $Q$. The two named hypotheses are the instances of that predicate at the edge stencil and at the axis stencil on the canonical encoded periodic Freudenthal torus (sizes strictly larger than 2).
The module already records exact $a^2$-homogeneity for both stencils and a rigidity lemma: any two homogeneous quadratics that both satisfy the local correspondence on the same complex are pointwise equal.
proof idea
One-line term application of reggeLocalQuadraticCorrespondence_quadratic_unique on the triangulation $K$ of the canonical encoded periodic Freudenthal torus. The two homogeneity witnesses are periodicEdgeStencilDirichletAction_smul and canonicalPeriodicMixedAxisStencilAction_smul. The legacy correspondence is rewritten via the Iff that identifies it with the general ReggeLocalQuadraticCorrespondence instance; the corrected correspondence is passed directly. Uniqueness then yields pointwise equality of the two actions on every vertex potential.
why it matters
This is the rigidity half of the Session 202 correction argument. Its sole downstream consumer is not_both_correspondences_of_quadratics_differ, which combines the present equality with the audit witness that the two stencils differ somewhere, and concludes mutual exclusivity: at most one of the legacy and corrected endpoints can be the true cubic-Taylor statement for the Regge action.
The module status is fully proved (zero sorry); the corrected gate itself remains named OPEN and is not asserted here. The result forces the choice of quadratic rather than treating the axis-stencil rewrite as aesthetic. It sits inside the gravity Track 1.B route that feeds the D2 damped-schedule residual bound, and thereby the continuum bridge identifying Laplacian action with hinge deficits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.