cubeAdmissible_forces_canonical
plain-language theorem explainer
At spatial dimension three, any torsion schedule that is cube-admissible (ground zero, second generation on passive edges, third on faces plus edges) equals the canonical generation torsion {0, 11, 17}. Mass and ledger authors cite it to replace a bare equality hypothesis by a structural premise. The proof rewrites to geometric torsion and discharges the three generation cases from the admissibility fields.
Claim. Fix spatial dimension $D = 3$. Let $\tau : \mathrm{Generation} \to \mathbb{Z}$ be any schedule satisfying the cube-admissible torsion axioms: $\tau(\mathrm{first}) = 0$, $\tau(\mathrm{second}) = E_{\mathrm{passive}}(D)$, and $\tau(\mathrm{third}) = E_{\mathrm{passive}}(D) + F(D)$. Then $\tau$ equals the canonical generation torsion schedule.
background
The Generation Torsion Bridge module derives the charged-generation torsion values ${0, 11, 17}$ from $Q_3$ cube combinatorics at the forced spatial dimension $D = 3$ (T8). Generation 1 is ground mode with no geometric coupling; generation 2 is edge-dressed with passive-edge count $E_{\mathrm{passive}}(D) = \mathrm{cube_edges}(D) - 1$; generation 3 is face-plus-edge dressed with $W_{\mathrm{endo}}(D) = E_{\mathrm{passive}}(D) + \mathrm{cube_faces}(D)$. At $D = 3$ these evaluate to $0$, $11$, and $17$ with no literal numerals in the geometric definition.
Cube-admissible torsion is the explicit structural premise that a schedule assigns exactly those three coupling modes. The module states this premise openly rather than burying it in comments, and certifies uniqueness of the solution together with pointwise agreement against the anchor integers and the RecogSpec schedule. The coupling rule itself is not yet derived from the Recognition Composition Law; the upgrade is from hardcoded numerals to a named uniqueness statement.
proof idea
Rewrite the goal via the sibling equality that geometric cube torsion coincides with canonical generation torsion. Apply functional extensionality on generations, then case-split.
The first-generation case is the admissibility field ground_is_zero. The second is edge_mode. The third simplifies the geometric definition through the endogenous weight $W_{\mathrm{endo}}$ and applies face_edge_mode. No arithmetic decision procedure is required; the three fields of the structure supply the values directly.
why it matters
This is the uniqueness engine of the torsion bridge: any schedule obeying the cube coupling modes is forced to the canonical schedule used throughout the mass ladder. Downstream, incremental_forces_canonical reduces the weaker incremental-filtration premise to this theorem, and rsLedger_torsion_from_cube replaces the bare ledger hypothesis $L.\mathrm{torsion} = \mathrm{generationTorsion}$ by cube-admissibility at $D = 3$.
In the framework this sits under the mass domain and the T8 forcing of three spatial dimensions. It does not close the remaining premise that fermion generations couple to cube features in ground / passive-edge / face-plus-edge order; that coupling is still structural until derived from the RCL or from the CW-filtration route in ExcitationOrdering. What it does close is the gap from raw integers to a uniqueness theorem under an explicit predicate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.