allCardinalityGate_implies_cubicGate
plain-language theorem explainer
If the corrected local-axis-stencil correspondence holds on every periodic Freudenthal torus with sides at least 3, then it holds on every cubic torus of side N ≥ 3. Gravity Track 1.B workers cite this as the trivial specialization half of the parameterized reduction. The proof is a one-line instantiation of the universal quantifier at equal sides (N,N,N).
Claim. Assume the corrected local Taylor correspondence with the axis stencil holds for every triple of side lengths $N_x,N_y,N_z\ge 3$ on the corresponding periodic Freudenthal tori. Then, for every integer $N\ge 3$, the same correspondence holds on the cubic torus of side $N$ (i.e., at $(N_x,N_y,N_z)=(N,N,N)$).
background
Track 1.B studies a corrected local-Taylor gate: a finite coefficient identity equating the axis-stencil action to a cubic Taylor model on a periodic Freudenthal torus. The sibling module closed the gate at $N=5$ by a native_decide certificate over the $5^3=125$ vertex table. The all-cardinality generalization (arbitrary sides $N_x,N_y,N_z\ge 3$) remains open.
This module isolates a uniform cubic identity: the corrected correspondence restricted to equal sides $N_x=N_y=N_z=N$. The all-cardinality gate is the statement that the correspondence holds for every valid triple of sides, not merely the cubic diagonal. The cubic gate at scale $N$ is exactly that correspondence evaluated at $(N,N,N)$; for each fixed $N$ it is again a finite identity over an $N^3$ table.
The local setting is pure reduction and algebra: no new certificates, only the logical relationship between the universal gate and its cubic specializations, plus an evenness lemma for homogeneous quadratics used as a necessary condition at every cardinality.
proof idea
Term-mode one-liner. The all-cardinality hypothesis is a universal quantifier over sides $N_x,N_y,N_z$ (each nonzero and strictly larger than 2) asserting the local correspondence. Instantiate all three side parameters by the same $N$ and all three lower-bound hypotheses by the given $hN:2<N$. The resulting proposition is definitionally the cubic gate at scale $N$. No lemmas, rewrites, or certificates are required.
why it matters
This is contribution (1) of the module: the forward half of the parameterized reduction between the open all-cardinality corrected gate and the family of cubic gates at every $N\ge 3$. Together with the reverse implication (stated as a separate proposition, not proved here) it yields the equivalence that the all-cardinality gate holds if and only if every cubic gate holds and the reverse analytic step is valid.
Downstream the cubic gate is the natural target for finite certificates (as already done at $N=5$). The forward reduction lets any future all-cardinality proof discharge every cubic instance for free. The reverse direction is flagged in-module as a nontrivial analytic step: correspondence at $(N,N,N)$ need not automatically give arbitrary $(N_x,N_y,N_z)$. No parent theorems currently consume this lemma (used_by is empty); it is infrastructure for closing the open all-cardinality gate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.