CanonicalPeriodicCorrectedTrack1BGateAtN5
plain-language theorem explainer
The corrected Track 1.B gate at N=5 is the finite coefficient identity for the explicit-fiber axis-stencil target. Second-order Schläfli stationarity at this scale is already a theorem, so corrected closure reduces exactly to that Prop. Gravity work on the axis-stencil local correspondence or the Session 202 weight correction cites it as the named gate hypothesis. The declaration is a pure abbreviation aliasing the target proposition.
Claim. The corrected Track 1.B gate at $N=5$ is the proposition that the explicit-fiber mixed hinge-deficit axis-stencil coefficient identity holds at the $N=5$ certificate scale.
background
Track 1.B targets a local Regge/J-cost correspondence in gravity, factoring through a mixed hinge-deficit quadratic. A Session 202 finite audit showed the legacy seven-class edge-stencil identification was wrong-weighted: at the $N=5$ single-vertex bump the mixed quadratic evaluates to 12, while the edge stencil evaluates to $6+6\sqrt{2}+2\sqrt{3}$. The corrected endpoint takes the rational axis stencil as the candidate quadratic.
This module supplies that corrected local correspondence, its quadratic algebra (nonnegativity, exact $a^2$-homogeneity), and rigidity: two homogeneous quadratics satisfying the correspondence on the same complex are pointwise equal. Thus at most one of the legacy and corrected endpoints can be the true Taylor coefficient; the audit selects the axis stencil. Second-order Schläfli stationarity at $N=5$ is already proved, so the remaining certificate-scale gate is the single finite coefficient identity named here.
proof idea
No proof content. The declaration is an abbreviation that equates the named gate proposition with the explicit-fiber axis-stencil target at $N=5$. Downstream discharge is separate: correctedTrack1BGateAtN5_closed applies the finite native_decide certificate from FreudenthalAxisStencilCoeffCert over the $125=5^3$ vertex table (with the documented compiler-trust axiom caveat).
why it matters
This gate is the named endpoint hypothesis for the corrected Track 1.B route after the Session 202 mismatch. The theorem correctedTrack1BGateAtN5_closed asserts it holds via the finite certificate. From a gate hypothesis, correctedMixedTargetAtN5_of_gate obtains the corrected mixed identification at $N=5$. Conditionally, correctedTrack1BGateAtCubic_five_of_gateImp lifts an implication from the gate to the cubic gate at $N=5$, reusing the certificate as a parameterized hypothesis rather than a bare re-export. In the broader gravity stack it closes the certificate-scale step of the axis-stencil local correspondence and feeds the parametric D2 damped-schedule residual bounds that depend on that correspondence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.