correctedTrack1BGateAtCubic_five_of_gateImp
plain-language theorem explainer
If the closed N=5 corrected Track 1.B coefficient identity implies the local cubic-Taylor axis-stencil correspondence on the side-5 Freudenthal torus, then that cubic correspondence holds. Gravity workers reducing the all-cardinality gate to finite cubic identities would cite this. Proof is one-line modus ponens feeding the existing native_decide N=5 certificate into the assumed implication.
Claim. Assume that the corrected Track 1.B gate at $N=5$ (the finite explicit-fiber axis-stencil coefficient identity) implies the local cubic-Taylor correspondence with the axis stencil on the cubic Freudenthal torus of side $5$. Then that cubic correspondence holds at $N=5$.
background
Track 1.B concerns the corrected local-Taylor identification between mixed hinge deficit and an axis stencil on periodic Freudenthal tori. The cubic gate at scale $N$ asserts that this local correspondence holds on the cubic torus of side $N$ (a finite coefficient identity over the $N^3$ vertex table). The all-cardinality gate asks for the same on every valid periodic torus, not only cubes.
The module packages a parameterized reduction: the cubic gate is defined uniformly as CorrectedTrack1BGateAtCubic N, and the all-cardinality statement is related to the family of cubic gates plus a reverse implication. Separately, the $N=5$ corrected gate (second-order Schläfli stationarity already proved) reduces to one finite coefficient identity, closed by a native_decide certificate over the $5^3=125$ table.
This declaration sits in the third contribution of the module: it reuses that closed $N=5$ certificate as the antecedent of a hypothesis, rather than re-exporting it standalone.
proof idea
Term-mode one-liner. The hypothesis hImp is an implication from the corrected $N=5$ gate to the cubic gate at $N=5$. Apply hImp to correctedTrack1BGateAtN5_closed, the theorem that discharges the $N=5$ gate via the Freudenthal axis-stencil coefficient certificate. No further rewriting or case analysis.
why it matters
Closes the conditional $N=5$ link advertised in the module purpose: the existing finite certificate is wired into the parameterized cubic-gate framework instead of remaining a one-off export. Downstream the module already has the all-cardinality $\Leftrightarrow$ (cubic-at-every-$N$ and reverse) equivalence and the algebraic evenness of homogeneous quadratics; this theorem supplies the concrete $N=5$ instance under an implication hypothesis.
It does not finish the open all-cardinality corrected gate. It only shows how a proved finite identity at the certificate scale lifts to the cubic gate once the local-correspondence implication is granted. In the broader RS gravity track this is bookkeeping on the corrected Taylor gate, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.