allCardinalityGate_iff_cubic_and_reverse
plain-language theorem explainer
The all-cardinality corrected Track 1.B gate is equivalent to the cubic gate holding at every side length N ≥ 3 together with the reverse implication from cubic to all-cardinality. Anyone reducing the open higher-cardinality correspondence cites this packaging. The proof is a two-direction constructor: specialize the triple (N,N,N), then apply the reverse hypothesis.
Claim. The statement that the corrected local-Taylor axis-stencil correspondence holds on every periodic Freudenthal torus with sides $N_x,N_y,N_z > 2$ is equivalent to the conjunction of (i) the same correspondence on every cubic torus of side $N \ge 3$, and (ii) the reverse implication: if the cubic case holds for all such $N$, then the general $(N_x,N_y,N_z)$ case follows.
background
This module sits in the Gravity Track 1.B line after the corrected quadratic local-Taylor gate. The $N=5$ cubic case was already closed by a finite native_decide certificate over the $5^3$ vertex table; the all-cardinality generalization remains open. The present file packages that open claim as a parameterized reduction.
The all-cardinality corrected gate asserts that the canonical periodic axis-stencil local correspondence holds for every triple of sides $N_x,N_y,N_z > 2$. The cubic gate at scale $N$ is the special case $N_x = N_y = N_z = N$, a finite coefficient identity on the $N^3$ vertex table. The reverse hypothesis is the nontrivial analytic claim that cubic success at every $N$ upgrades to arbitrary rectangular tori.
The module purpose states three contributions: the parameterized reduction (this equivalence and the forward implication), an algebraic evenness lemma for homogeneous quadratics (needed at every cardinality because the Regge action is even about the flat critical point), and a conditional $N=5$ bridge that reuses the existing certificate as a hypothesis rather than a standalone export.
proof idea
Pure term-mode constructor on the biconditional; no external lemmas.
Left-to-right: assume the all-cardinality gate $h$. The cubic family is obtained by specializing $h$ at $(N,N,N)$ for each $N > 2$. The reverse implication is recovered by feeding an arbitrary cubic family back into $h$ (the cubic family is already an instance of the all-cardinality statement once the sides are equal).
Right-to-left: given a cubic family $h_{\mathrm{cub}}$ and a reverse implication $h_{\mathrm{rev}}$, apply $h_{\mathrm{rev}}$ to $h_{\mathrm{cub}}$.
The argument is purely propositional packaging of the two directions already isolated as allCardinalityGate_implies_cubicGate and CubicGateImpliesAllCardinality.
why it matters
In the Recognition gravity stack this is the clean interface that reduces the open all-cardinality corrected Track 1.B gate to one uniform finite identity (the cubic gate at every $N \ge 3$) plus a single reverse analytic implication. The module doc lists it explicitly as contribution (1) of the parameterized reduction.
Downstream use is not yet wired (no used_by edges), so the declaration is presently a packaging theorem rather than a leaf of a larger proved chain. It does not touch the forcing chain T0–T8, the Recognition Composition Law, or the $\phi$-ladder mass formula; its role is local to the Regge/Freudenthal axis-stencil correspondence that underwrites the corrected quadratic gravity gate.
The open question it isolates is precisely CubicGateImpliesAllCardinality: whether cubic success upgrades to rectangular tori. Closing that implication, together with certificates for the cubic gate at each $N$, would discharge the all-cardinality gate entirely.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.