AllCardinalityCorrectedGate
plain-language theorem explainer
Defines the all-cardinality corrected Track 1.B gate: the local axis-stencil correspondence holds on every valid periodic Freudenthal torus with side lengths at least 3, not only the cubic case. Gravity and discrete-Regge workers cite it as the uniform target that the cubic-parameterized reductions aim at. The body is a pure universal quantification over the existing local-correspondence predicate; no proof work lives here.
Claim. The all-cardinality corrected gate is the proposition that for every triple of positive integers $N_x, N_y, N_z$ each strictly larger than $2$, the corrected local correspondence between the rational axis stencil and the mixed hinge-deficit quadratic holds on the canonical encoded periodic Freudenthal torus of those side lengths.
background
Track 1.B concerns a local Taylor-type match on periodic Freudenthal tori: the rational axis stencil should equal the Session-202-corrected mixed hinge-deficit quadratic. Upstream, CanonicalPeriodicAxisStencilLocalCorrespondence packages that match as ReggeLocalQuadraticCorrespondence on the canonical encoded torus of sides $(N_x,N_y,N_z)$ with each side $>2$.
The parent module already closed a finite certificate at the cubic $N=5$ case via native_decide over the $5^3$ vertex table. The open step is the uniform statement for every admissible torus, cubic or not. This definition names that uniform statement so later lemmas can reduce it to a one-parameter cubic family plus a reverse implication.
Side constraints $N_i\ge 3$ and NeZero match the geometry hypotheses of the encoded periodic torus construction; they are not extra physics assumptions.
proof idea
Definitional packaging only. The proposition is the universal closure of the upstream local-correspondence predicate over all admissible side triples $(N_x,N_y,N_z)$. No tactics, no certificates, no algebraic reduction: the body is literally that quantified Prop.
why it matters
This is the named target of the higher-cardinality program in the corrected Taylor gate. Downstream, the forward reduction shows it implies the cubic gate at every $N\ge 3$ by specializing $N_x=N_y=N_z=N$. The reverse direction is left as an explicit proposition (cubic-at-all-$N$ implies all-cardinality), and the equivalence theorem factors the full gate into the cubic family plus that reverse implication.
In the Recognition gravity stack this sits on the discrete Regge / Freudenthal side of the corrected quadratic endpoint, not on the T0–T8 forcing chain or the mass ladder. It does not close the open all-cardinality analytic step; it only gives the reductions a single Prop to talk about. Module status still records the all-cardinality generalization as open outside the cubic $N=5$ certificate path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.