not_both_correspondences_of_quadratics_differ
plain-language theorem explainer
On a periodic Freudenthal torus with each side at least 3, if the legacy edge-stencil quadratic and the corrected axis-stencil quadratic disagree at some vertex potential, then the two local Regge cubic-Taylor correspondences cannot both hold. Track 1.B gravity work cites this as exclusivity of the legacy seven-class endpoint versus the Session-202 axis endpoint. Proof is a short contradiction via quadratic rigidity.
Claim. Let $N_x,N_y,N_z\ge 3$. Suppose there is a vertex potential $\xi$ on the canonical periodic Freudenthal torus such that the seven-class edge-stencil Dirichlet action at $\xi$ differs from the mixed axis-stencil action at $\xi$. Then the legacy edge-stencil local correspondence and the corrected axis-stencil local correspondence cannot both hold on that complex.
background
Track 1.B factors the local Regge/J-cost correspondence through a mixed hinge-deficit quadratic on a periodic Freudenthal triangulation. The legacy endpoint took the seven-class square-root edge stencil as that quadratic. Session 202's exact finite audit found a wrong weighting: at the $N=5$ single-vertex bump the mixed quadratic is $12$, while the edge stencil is $6+6\sqrt{2}+2\sqrt{3}$.
The corrected endpoint uses the rational axis stencil already identified with the mixed hinge-deficit quadratic. Local cubic-Taylor correspondence is stated for an arbitrary homogeneous candidate quadratic $Q$. The difference hypothesis is the named proposition that those two stencil actions disagree somewhere (the Session 202 audit witness, packaged as a Prop).
Rigidity upstream says any two homogeneous quadratics realizing the correspondence on the same complex are pointwise equal; the joint-satisfiability corollary is that both endpoints force the stencils to coincide.
proof idea
Term-mode contradiction. Introduce both correspondences (legacy edge stencil and corrected axis stencil). From the difference hypothesis obtain a concrete vertex potential $\xi$ where the two quadratic actions disagree. Feed both correspondences into the rigidity corollary that joint satisfaction forces the two homogeneous quadratics to agree at every potential, including $\xi$. That forced equality contradicts the witness inequality at $\xi$.
why it matters
Exclusivity corollary of Track 1.B quadratic rigidity: given the Session 202 mismatch witness, at most one of the legacy seven-class endpoint and the corrected axis endpoint can be the true cubic-Taylor statement for the Regge action; the audit selects the axis stencil. The module proves the corrected endpoint definition, axis-stencil algebra, and the parametric D2 residual bound so the damped-schedule pipeline can transfer once the corrected gate closes. That gate remains named OPEN, not asserted. No downstream uses are wired yet; the lemma is the logical force behind preferring the correction over aesthetics. It sits in the gravity Track 1.B route toward local Regge/J-cost correspondence, not in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.