CanonicalPeriodicAxisStencilLocalCorrespondence
plain-language theorem explainer
Names the corrected Track 1.B endpoint: the local cubic-Taylor correspondence between the Regge action and the rational axis stencil on a periodic Freudenthal torus with side lengths greater than 2. Gravity workers on the mixed hinge-deficit route cite this as the Session-202 gate proposition. It is a one-line specialization of the general local-quadratic correspondence at the audit-selected quadratic.
Claim. For $N_x,N_y,N_z\in\mathbb{N}$ with each side strictly larger than $2$, write $T$ for the canonical encoded periodic Freudenthal torus of those sides. The corrected Track 1.B endpoint is the assertion that the local cubic-Taylor correspondence holds on $T$ when the candidate quadratic is the rational mixed-axis stencil action (the Session-202 identification of the mixed hinge-deficit quadratic).
background
Track 1.B factors the local Regge/J-cost correspondence through a mixed hinge-deficit quadratic on a periodic Freudenthal torus (a cubic lattice complex with periodic boundary data and a fixed six-tetrahedron cell). The general predicate is the local cubic-Taylor correspondence for an arbitrary candidate quadratic $Q$ on that complex: the second-order expansion of the nonlinear Regge action must match $Q$ at every admissible vertex potential.
Session 202's exact finite audit showed the legacy seven-class square-root edge stencil is wrong-weighted. At the $N=5$ single-vertex bump the mixed quadratic evaluates to $12$, while the seven-class stencil evaluates to $6+6\sqrt{2}+2\sqrt{3}$; those scalars differ. The corrected identification equates the mixed quadratic with the rational axis stencil (twice the axis-edge stencil, with local square-root factors cancelled).
The dimensionless bridge ratio $K=\varphi^{1/2}$ enters only as the complex's built-in scale datum. This definition packages the corrected endpoint: correspondence at that axis stencil on the canonical encoded torus.
proof idea
Pure abbreviation, no proof obligations. It feeds the torus's built-in $K$ and $K$-hypothesis, together with the canonical periodic mixed-axis stencil action, into the general local-quadratic correspondence predicate. Downstream theorems treat the resulting Prop as a named hypothesis or as the body of a gate.
why it matters
This is the corrected Track 1.B endpoint the module exists to supply. Downstream, the cubic gate is exactly this proposition on the equal-side torus, and the all-cardinality gate is the universal quantification over all valid side triples. Inside the module it is the hypothesis of the axis-normalized residual bound that hooks the damped D2 schedule, and of the rigidity pair: both legacy and corrected correspondences force the two stencils to agree pointwise, hence (given the Session-202 mismatch witness) they are mutually exclusive.
The module status is explicit: everything stated here is theorem-grade (0 sorry), but the corrected gate itself is named OPEN and not asserted. Closing that gate is the remaining finite coefficient identity over the vertex table. In the broader RS gravity stack this is the local cubic-Taylor step that feeds continuum residual control; it does not itself touch T5–T8 or the RCL, only the discrete Regge side of the correspondence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.