correctedTrack1BGateAtN5_closed
plain-language theorem explainer
The corrected Track 1.B gate at lattice size N=5 is closed: the explicit-fiber mixed hinge-deficit equals the axis-stencil target coefficient. Gravity and Regge-calculus workers cite it as the finite certificate that finishes the corrected local correspondence endpoint. The proof is a one-line term re-export of the Freudenthal native_decide certificate over the 5³ vertex table.
Claim. The corrected Track 1.B gate at $N=5$ holds: the explicit-fiber mixed hinge-deficit axis-stencil coefficient identity is true on the periodic $N=5$ complex (equivalently, second-order Schl\"afli stationarity already being known, the single remaining finite coefficient match is satisfied).
background
Track 1.B aims at a local Regge/J-cost correspondence on the periodic cubic complex. Session 202 showed the legacy mixed hinge-deficit identification was wrong-weighted: at the $N=5$ single-vertex bump the mixed quadratic evaluates to $12$, while the seven-class square-root edge stencil evaluates to $6+6\sqrt{2}+2\sqrt{3}$, and those scalars are proved unequal. The corrected endpoint replaces that with the rational axis stencil as the candidate quadratic.
Because second-order Schl"afli stationarity at $N=5$ is already a theorem, the corrected gate reduces to one finite coefficient identity: the explicit-fiber axis-stencil target. That identity is packaged as the proposition abbreviated by the gate name in this module.
Upstream, canonicalPeriodicMixedHingeDeficitExplicitFiberAxisStencilTargetAtN5 in FreudenthalAxisStencilCoeffCert closes the target from a finite coefficient certificate plus a real/coefficient soundness bridge, via native_decide on the $125=5^3$ vertex table.
proof idea
One-line term proof: the gate proposition is definitionally the explicit-fiber axis-stencil target at $N=5$, so the theorem is exactly the already-proved Freudenthal certificate
canonicalPeriodicMixedHingeDeficitExplicitFiberAxisStencilTargetAtN5,
itself obtained from coefficient soundness at $N=5$ plus the soundness bridge. No extra algebra is done here; this declaration only names the closed gate for downstream Track 1.B status and cubic-cardinality hooks.
why it matters
This is the named closure of the corrected $N=5$ endpoint for Track 1.B after the Session 202 mismatch forced the axis-stencil correction. Downstream, correctedTrack1BGateAtCubic_five_of_gateImp consumes it as the hypothesis that turns a gate-implies-cubic implication into the cubic gate at $N=5$. The module status record and track1BCompilerTrustStatus point at it as the closed, compiler-trusted certificate (extra axioms Lean.ofReduceBool and Lean.trustCompiler on top of the standard kernel basis), while recording that the all-cardinality generalization remains open.
In the broader Recognition gravity stack it anchors the corrected local quadratic correspondence used by the D2 damped-schedule residual bound, so the Taylor coefficient that feeds higher-cardinality and compiler-trust reporting is the axis stencil rather than the legacy edge stencil.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.