cubeAdmissible_unique
plain-language theorem explainer
Any torsion schedule that is cube-admissible at dimension d is forced to the unique geometric assignment: ground 0, second generation passive edges, third generation passive edges plus faces. Mass and generation authors cite it to replace ad-hoc τ values by a uniqueness statement under an explicit coupling premise. The proof is a three-case funext on Generation, reading the three fields of the admissibility structure.
Claim. For any dimension $d\in\mathbb{N}$ and any schedule $\tau:\mathrm{Generation}\to\mathbb{Z}$, if $\tau$ is cube-admissible at $d$ (ground mode zero, second generation equal to the passive-field edge count $E_{\mathrm{passive}}(d)$, third generation equal to $E_{\mathrm{passive}}(d)+F(d)$ with $F(d)=2d$ faces), then $\tau$ equals that geometric schedule pointwise.
background
The module Generation Torsion Bridge is the authoritative geometric derivation of charged-generation torsion from $Q_3$ cube combinatorics. At spatial dimension $D=3$ (forced by the linking/T8–T9 chain), the intended integers are $\tau=(0,11,17)$: ground uncoupled, second generation dressed by passive field edges, third by passive edges plus faces.
Cube geometry supplies the counts without raw numerals: $\mathrm{cube_faces}(d)=2d$, and $\mathrm{passive_field_edges}(d)$ is total cube edges minus the single active edge per tick (so $11$ at $D=3$). Cube-admissible torsion is the explicit structural premise that generations couple in ground / edge / face+edge modes to those counts. The module states this as a Prop structure rather than burying the rule in comments, upgrading hardcoded numerals to a named hypothesis with uniqueness.
That premise is not yet derived from the Recognition Composition Law alone; it encodes how fermion generations attach to cube features. A stronger CW-filtration route appears in ExcitationOrdering.
proof idea
Term-mode uniqueness by extensionality. Apply funext on the generation argument, then case-split on the three constructors of Generation. Each case is definitionally the corresponding field of the hypothesis CubeAdmissibleTorsion d τ: ground uses ground_is_zero, second uses edge_mode (equality to passive_field_edges d), third uses face_edge_mode (equality to passive_field_edges d + cube_faces d). No auxiliary lemmas are needed beyond the structure projections.
why it matters
This is the forcing half of the module's certification list: an explicit structural predicate whose unique solution is the geometric schedule built from cube arithmetic. Together with siblings that identify cube geometric torsion with Anchor and RecogSpec generation torsion, it closes the "no raw numerals" and "unique under admissibility" claims for ${0,11,17}$.
In the broader RS mass story, generation torsion enters the $\varphi$-ladder mass formula via rung gaps. Here the integers come from $E_{\mathrm{passive}}+F$ at $D=3$ (T8 spatial dimension), not from fitting. The endogenous third-generation value $11+6=17$ numerically matches the crystallographic wallpaper count, but the primary source in this module is cube arithmetic.
No downstream users are wired yet in the graph. The remaining open premise is the physical coupling rule itself: until edge-before-face dressing is forced from the RCL or from the CW filtration of $Q_3$, the gap is "explicit structural premise plus uniqueness," not a pure cost-functional theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.