RCLForcedTorsion
plain-language theorem explainer
A torsion schedule τ on the three particle generations is RCL-forced in dimension d when it arises from coupling profiles that obey the CW boundary prerequisite, start uncoupled at the ground generation, climb the edge-then-face filtration, and match profile torsion at each generation. Mass and generation papers cite this predicate as the forcing interface. It is a pure existence Prop, not a proved uniqueness statement.
Claim. A map $\tau$ from the three generations to integers is RCL-forced in dimension $d$ if there exist coupling profiles (one per generation) such that: each profile satisfies the CW boundary prerequisite; the first generation is fully uncoupled; the second couples only the edge channel; the third couples both edge and face channels; and $\tau(g)$ equals the profile torsion of that generation's profile in dimension $d$.
background
The module derives the generation torsion schedule ${0,11,17}$ as the unique values compatible with the 8-tick Hamiltonian cycle on the 3-cube $Q_3$, projected onto the $\varphi$-ladder through the Recognition Composition Law. RCL in log-coordinates becomes d'Alembert's equation; its solution $J=\cosh-1$ makes independent coupling contributions add in the ladder exponent.
The 8-tick Gray cycle visits all vertices of $Q_3$. At each tick one edge is active and the passive skeleton partitions into CW levels (edges, then faces). The CW attachment rule forces a boundary prerequisite: any profile that couples faces must already couple edges, so admissible profiles form a lower set in the CW poset. Variational dynamics pins the ground generation to the zero-cost uncoupled profile.
Spatial dimension is the forced value $D=3$ (T8). Coupling profiles are boolean pairs recording edge and face activation; profile torsion converts a profile into an integer ladder offset in dimension $d$. This definition packages those constraints into a single predicate on schedules $\tau$.
proof idea
Definitional, not a proof. The body is an existential Prop: witnesses are maps from generations to coupling profiles, conjoined with the four forcing clauses (CW prerequisite on every profile, fixed filtration values $\langle\mathrm{false},\mathrm{false}\rangle$, $\langle\mathrm{true},\mathrm{false}\rangle$, $\langle\mathrm{true},\mathrm{true}\rangle$ on the three generations, and pointwise equality of $\tau$ with profile torsion). Downstream theorems discharge the existential by exhibiting the canonical profiles and invoking uniqueness lemmas.
why it matters
This predicate is the forcing interface for the torsion schedule in the Masses chain. The main uniqueness theorem rcl_forced_torsion_unique states that any $\tau$ satisfying it at $D=3$ equals the canonical generation torsion ${0,11,17}$, citing T5 (RCL uniqueness / additive channels), T7 (eight-tick cycle), CW topology of $Q_3$, and variational ground-state zero.
Immediate parents: existence of a witness for the canonical schedule; uniqueness and exists-unique packaging; implications that RCL-forced schedules are cube-admissible, incremental, and filtration-compatible; the ledger bridge that reads torsion from RCL; and the module certificate TorsionForcingCert. Together they close the structural gap between the 8-tick geometry and the mass-ladder offsets used downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.