rcl_forced_implies_cubeAdmissible
plain-language theorem explainer
Any integer torsion schedule on the three fermion generations that admits an RCL-forced coupling witness at spatial dimension three is automatically cube-admissible: ground torsion vanishes, the second generation sits at the passive-edge count, and the third adds the face count. Mass and generation papers cite this to pass from the RCL/CW forcing package to the geometric torsion values {0,11,17}. The proof is a two-line term: uniqueness rewrites the schedule to the canonical generation torsion, which is already known admissible.
Claim. Let $\tau:\{\mathrm{gen}_1,\mathrm{gen}_2,\mathrm{gen}_3\}\to\mathbb{Z}$. If $\tau$ is RCL-forced at $D=3$ (there exist coupling profiles, one per generation, that obey the CW prerequisite, start from the uncoupled ground profile, advance through the CW filtration in dimensional order, and reproduce $\tau$ as profile torsion), then $\tau$ is cube-admissible: $\tau(\mathrm{gen}_1)=0$, $\tau(\mathrm{gen}_2)=E_{\mathrm{passive}}(3)$, and $\tau(\mathrm{gen}_3)=E_{\mathrm{passive}}(3)+F(3)$.
background
The module TorsionForcing closes the structural gap that pins generation torsion to the discrete set {0, 11, 17}. The chain is: Recognition Composition Law forces additive torsion channels on the φ-ladder; the 8-tick Hamiltonian cycle on the 3-cube Q₃ partitions edges and faces into active versus passive subcells; CW attachment forces coupling profiles to be downward-closed in the cell poset; variational ground-state cost forces zero torsion at generation one.
RCL-forced torsion is the existence package for those profiles: each generation has a coupling profile satisfying the CW prerequisite, the first profile is fully uncoupled, the second turns on edges only, the third turns on edges and faces, and τ equals the profile torsion at every generation. Cube-admissible torsion is the purely numerical counterpart: ground mode zero, edge mode equal to the passive-edge count, face-plus-edge mode equal to passive edges plus faces.
Upstream, generationTorsion_admissible already shows the canonical schedule is cube-admissible at D = 3 (via equality with geometric cube torsion). Spatial dimension D = 3 is the T8/T9 landmark used throughout the mass sector.
proof idea
Term-mode, two steps. First rewrite the goal along the uniqueness theorem for RCL-forced torsion: any τ satisfying the RCL-forced package equals the canonical generation torsion schedule. After that rewrite the goal is exactly cube-admissibility of generation torsion, which is the upstream lemma generationTorsion_admissible. No case analysis on generations is repeated here.
why it matters
This is the bridge from the RCL-plus-CW forcing witness to the structural premise used by the mass ladder. Cube admissibility is the explicit numerical statement that generation torsions are 0, then passive edges, then passive edges plus faces; at D = 3 those integers are 0, 11, 17, the values the module title advertises. The module derivation chain (A)–(E) treats RCL additivity, the 8-tick Gray cycle on Q₃, CW lower-set constraints, and variational ground zero as the forcing inputs; this theorem packages the output as cube admissibility.
Framework landmarks in play: T8 forces D = 3, T7 supplies the eight-tick octave whose Hamiltonian cycle partitions Q₃, and the Recognition Composition Law supplies the additive torsion channels on the φ-ladder. No downstream consumers are wired yet in the graph, so the lemma currently stands as a terminal closure fact inside TorsionForcing rather than an intermediate hop into a larger mass theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.