CubeAdmissibleTorsion
plain-language theorem explainer
A torsion schedule τ on the three fermion generations is cube-admissible at dimension d when gen-1 is uncoupled (τ=0), gen-2 equals the passive-edge count E_passive(d), and gen-3 equals E_passive(d)+F(d). Mass and generation authors cite it as the explicit structural premise that replaces hardcoded {0,11,17}. It is a Prop-valued structure with three field equations; no proof body.
Claim. A map $\tau$ from the three generations to integers is cube-admissible at dimension $d$ when $\tau(\mathrm{gen}_1)=0$, $\tau(\mathrm{gen}_2)=E_{\mathrm{passive}}(d)$, and $\tau(\mathrm{gen}_3)=E_{\mathrm{passive}}(d)+F(d)$, where $E_{\mathrm{passive}}(d)$ is the number of passive field edges of the $d$-cube and $F(d)=2d$ is the number of faces.
background
The Generation Torsion Bridge module derives the charged-generation torsion schedule from $Q_3$ cube combinatorics and proves agreement with every other representation in the codebase (Anchor integers, RecogSpec generation torsion, CW-cumulative torsion). The intended values at spatial dimension $D=3$ are ${0,11,17}$.
Cube geometry supplies the integers without raw numerals: passive field edges $E_{\mathrm{passive}}(d)$ equal total cube edges minus one active edge per tick (at $d=3$ this is 11), and faces are $F(d)=2d$ (at $d=3$ this is 6). The third-generation endogenous winding is then $W_{\mathrm{endo}}(d)=E_{\mathrm{passive}}(d)+F(d)=17$ at $D=3$. Spatial dimension $D=3$ is the value forced by the forcing chain (T8).
The module states explicitly that the ground / passive-edge / face+edge assignment rule is a structural premise about how fermion generations couple to cube features, not yet a consequence of the Recognition Composition Law alone. This structure packages that premise as a named predicate rather than burying it in comments.
proof idea
No proof: this is a Prop-valued structure definition. Its three fields are literal equalities fixing $\tau$ on the three generation constructors. Downstream theorems inhabit it by rfl or short rewrites against cubeGeometricTorsion and W_endo (see cubeGeoTorsion_admissible), or discharge uniqueness by case analysis on Generation.
why it matters
This predicate is the forcing interface for the torsion bridge. Uniqueness (cubeAdmissible_unique) and the $D=3$ canonical-forcing theorem (cubeAdmissible_forces_canonical) show any admissible schedule equals the geometric schedule and hence generationTorsion. Ordering (cubeAdmissible_ordered) follows from cube arithmetic once $d\ge 2$. Equivalence to the incremental two-step filtration (cubeAdmissible_iff_incremental) and the CW route (cwTorsion_cubeAdmissible in ExcitationOrdering) certify that geometric, ledger, and filtration presentations coincide.
In framework terms it upgrades the gap from hardcoded numerals ${0,11,17}$ to an explicit structural premise with a uniqueness proof, while leaving open the deeper derivation of the ground/edge/face coupling rule from the RCL. The eight-tick octave and $D=3$ enter only through the cube counts that instantiate the fields at the physical dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.