CubicGateImpliesAllCardinality
plain-language theorem explainer
Names the reverse reduction hypothesis: if the corrected Track-1B cubic gate holds at every side length N ≥ 3, then the all-cardinality corrected gate follows. Gravity workers cite it when packaging the open higher-cardinality step as one implication beside the uniform cubic family. It is a pure Prop abbreviation, not a proved implication.
Claim. Let $G_{\mathrm{cubic}}(N)$ be the corrected Track-1B correspondence on the cubic Freudenthal torus of side $N\ge 3$, and let $G_{\mathrm{all}}$ be the corrected gate at arbitrary cardinalities $(N_x,N_y,N_z)$. The reverse-reduction proposition asserts $$\bigl(\forall N\ge 3,\; G_{\mathrm{cubic}}(N)\bigr)\;\Rightarrow\; G_{\mathrm{all}}.$$
background
The parent module packages the still-open all-cardinality extension of the corrected local-Taylor (Track-1B) gate. Track1BCorrectedQuadratic already closed the finite certificate at $N=5$ by native decision over the $5^3=125$ vertex table. Here the goal is a parameterized reduction: replace a single global statement by a uniform family of cubic identities plus one reverse arrow.
CorrectedTrack1BGateAtCubic N is the corrected correspondence restricted to the cubic Freudenthal torus of side $N$ (with $N\ge 3$ and $N\ne 0$). AllCardinalityCorrectedGate is the full statement at arbitrary positive cardinalities $(N_x,N_y,N_z)$. The forward direction (all-cardinality implies every cubic instance) is already a theorem in this module; the reverse direction is the nontrivial analytic step of lifting diagonal data $(N,N,N)$ to rectangular data.
This declaration simply records that reverse arrow as a named proposition, so the equivalence theorem can conjoin it with the cubic family without inlining a long implication type.
proof idea
No proof: the declaration is a def equal to a single implication type. The antecedent is the universal cubic gate (for every $N:\mathbb{N}$ with NeZero N and $2<N$, the corrected cubic identity at that $N$). The consequent is AllCardinalityCorrectedGate. Lean stores the Prop; nothing is discharged.
why it matters
It is the missing half of the parameterized reduction advertised in the module purpose. Downstream, allCardinalityGate_iff_cubic_and_reverse proves that the all-cardinality gate is equivalent to the conjunction of (a) the cubic gate at every $N\ge 3$ and (b) this reverse implication. That equivalence reduces an open global identity to one uniform finite family plus a single analytic lift from cubes to rectangular tori.
In the Recognition gravity stack this sits after the $N=5$ native_decide certificate and beside the algebraic evenness lemma for homogeneous quadratics. Closing the reverse arrow would finish the higher-cardinality corrected Taylor gate; until then the name isolates exactly which implication remains open. No T0–T8 forcing step is claimed here; the link is local to Track-1B stencil correspondence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.