CorrectedTrack1BGateAtCubic
plain-language theorem explainer
The corrected Track 1.B gate on a cubic Freudenthal torus of side N (N ≥ 3): the local cubic-Taylor correspondence with the axis stencil holds when all three periods equal N. Discrete-gravity workers cite it as the uniform finite identity that the all-cardinality gate reduces to at every scale. The body is a one-line specialization of the general three-period correspondence to equal periods (N,N,N).
Claim. For every natural number $N \ge 3$, the corrected Track 1.B cubic gate at scale $N$ asserts that the local cubic-Taylor correspondence between the corrected Track 1.B functional and the canonical periodic axis stencil holds on the cubic Freudenthal torus of side length $N$ (periods $(N,N,N)$). For each fixed $N$ this is a finite coefficient identity over the $N^3$ vertex table.
background
Track 1.B concerns a corrected local-Taylor expansion matched to a canonical periodic axis stencil on Freudenthal tori. The parent module closed that correspondence at the single scale $N=5$ by a native_decide certificate over the $5^3=125$ vertex table. The all-cardinality statement (the same correspondence for every valid triple of periods $(N_x,N_y,N_z)$ with each $N_i\ge 3$) remains open.
This module isolates a uniform cubic slice: fix equal periods $N_x=N_y=N_z=N$ and ask only whether the local correspondence holds on that cubic torus. The general three-period predicate is CanonicalPeriodicAxisStencilLocalCorrespondence; the cubic gate is exactly that predicate at $(N,N,N)$. For each concrete $N$ the claim is a finite algebraic identity on the $N^3$ vertex table, not an analytic continuum statement.
The surrounding development also records an algebraic necessity condition (any exactly quadratically homogeneous real functional is even) and a conditional bridge that reuses the existing $N=5$ certificate inside the parameterized framework.
proof idea
Definition, not a proof. The body is the one-line specialization
CanonicalPeriodicAxisStencilLocalCorrespondence N N N hN hN hN,
i.e. the general three-period local-correspondence predicate evaluated on equal periods with the three side-length hypotheses all equal to the single assumption $2<N$. No tactics, no certificates, no algebraic rewriting.
why it matters
This definition is the uniform finite identity around which the higher-cardinality reduction is organized. Downstream, the all-cardinality gate implies the cubic gate at every $N\ge 3$ by restriction to equal periods (allCardinalityGate_implies_cubicGate). The reverse direction is packaged as the open proposition CubicGateImpliesAllCardinality. Their conjunction is equivalent to the full all-cardinality gate (allCardinalityGate_iff_cubic_and_reverse), so closing the cubic family plus one analytic reverse step would finish the generalization.
A separate conditional lemma (correctedTrack1BGateAtCubic_five_of_gateImp) shows that if the already-certified $N=5$ coefficient identity implies the local correspondence at $N=5$, then the cubic gate at $N=5$ follows. In the Recognition gravity stack this is the parameterized bridge from the single-scale Track 1.B certificate toward a scale-free discrete Taylor gate on periodic Freudenthal geometry; it does not itself touch the T0–T8 forcing chain or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.