AxisEdgeStencilQuadraticsDiffer
plain-language theorem explainer
Names the proposition that the legacy seven-class edge stencil and the corrected mixed axis stencil disagree as quadratic forms on some vertex potential of the canonical periodic Freudenthal torus (grid sizes > 2). Packages the Session 202 audit mismatch as a reusable hypothesis. Downstream exclusivity cites it to rule out joint satisfaction of both local cubic-Taylor correspondences. Body is a bare existential inequality, not a proof.
Claim. For integers $N_x,N_y,N_z>2$, the two stencils differ somewhere: there exists a vertex potential $\xi$ on the canonical encoded periodic Freudenthal torus such that the periodic edge-stencil Dirichlet action of $\xi$ is not equal to the canonical periodic mixed axis-stencil action of $\xi$.
background
Track 1.B aims at a local cubic-Taylor correspondence between the Regge action and a J-cost quadratic on a discrete 3-complex. The complex here is the canonical encoded periodic Freudenthal torus of sizes $N_x,N_y,N_z>2$; vertex potentials are real assignments to its vertices used as test fields for quadratic actions.
Session 202's finite audit showed the legacy identification was wrong-weighted: at the $N=5$ single-vertex bump the mixed hinge-deficit quadratic evaluates to $12$, while the seven-class square-root edge stencil evaluates to $6+6\sqrt{2}+2\sqrt{3}$. The corrected endpoint replaces that edge stencil by the rational axis stencil (mixed quadratic equal to the axis stencil).
This definition does not prove the mismatch. It names the content of the audit witness as a proposition: existence of some potential where the two candidate quadratics disagree pointwise as real numbers.
proof idea
Definitional packaging only. The body is the existential statement that there is a vertex potential $\xi$ on the torus for which periodicEdgeStencilDirichletAction and canonicalPeriodicMixedAxisStencilAction return unequal reals. No tactics, no lemmas applied; the Prop is the witness shape consumed by the exclusivity corollary.
why it matters
Feeds the exclusivity theorem not_both_correspondences_of_quadratics_differ: given this difference hypothesis, the legacy edge-stencil local correspondence and the corrected axis-stencil local correspondence cannot both hold. That corollary rests on rigidity (reggeLocalQuadraticCorrespondence_quadratic_unique): two homogeneous quadratics satisfying the same cubic-Taylor correspondence on one complex are pointwise equal, so distinct stencils cannot both be the true Taylor coefficient.
In the module narrative, the audit selects the axis stencil as the corrected Track 1.B endpoint. The gate itself remains named OPEN (not asserted here). The construction sits in the gravity track that links discrete Regge quadratics to Recognition J-cost structure; it does not itself invoke T5–T8 or the RCL identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.