TorsionForcingCert
plain-language theorem explainer
The torsion forcing certificate packages the structural conditions that uniquely force the generation torsion schedule {0, 11, 17}. Mass-ladder work cites it for the 8-tick Hamiltonian cycle on Q₃, the 11 passive edges plus 6 faces partition, CW edge-before-face ordering, three generation slots, and uniqueness of the RCL-forced torsion map. It is a Prop structure bundling those fields; the companion theorem discharges each one.
Claim. A torsion forcing certificate asserts: (i) the 3-cube admits a bijective Gray-code Hamiltonian path of period 8; (ii) at spatial dimension $D=3$, passive field edges equal 11 and cube faces equal 6; (iii) the coupling profile with faces on and edges off fails the CW boundary prerequisite; (iv) opposite face-pairs at dimension 3 equal 3; (v) there is a unique schedule $\tau:\mathrm{Generation}\to\mathbb{Z}$ that is RCL-forced at $D$; (vi) every such $\tau$ equals the canonical generation torsion $\{0,11,17\}$.
background
This module closes the structural gap for generation torsion on the φ-ladder. The Recognition Composition Law (RCL) has solution $J=\cosh-1$, so independent couplings add in the ladder exponent: $\varphi^a\cdot\varphi^b=\varphi^{a+b}$. Torsion values are therefore integer sums of passive subcell counts, not free parameters.
The 8-tick Gray cycle on $Q_3$ (T7) visits all $2^3$ vertices. At each tick one edge is active, leaving 11 passive field edges and 6 faces on the skeleton (passive_field_edges D = 11, cube_faces D = 6). Spatial dimension is fixed at $D=3$ (T8). Opposite face-pairs equal $D$, so three generation slots.
The CW prerequisite states that face coupling implies edge coupling: 2-cells attach along 1-cells, so a faces-only profile is geometrically incoherent. An RCL-forced torsion schedule is then a map $\tau$ witnessed by coupling profiles that obey CW, start uncoupled at the ground generation (zero J-cost), climb the CW filtration in order, and match profile torsion at each generation.
proof idea
No proof body: this is a structure-as-Prop. Six fields name the independent ingredients the companion theorem must supply. hamiltonian_cycle demands a bijective Gray path on the 3-cube. passive_partition hard-codes the $D=3$ counts 11 and 6. cw_prerequisite asserts that faces-without-edges is not a valid coupling profile. three_generations is the face-pair count identity at dimension 3. unique_schedule and schedule_is_canonical together demand a unique RCL-forced torsion map, equal to the canonical schedule. Downstream, each field is filled by a named lemma (Gray-cycle existence, native arithmetic, the CW violation lemma, rfl, and the uniqueness theorem for RCL-forced torsion).
why it matters
Parent theorem torsion_forcing_certificate is the sole direct consumer: it builds an inhabitant of this certificate and thereby asserts that the schedule {0, 11, 17} is forced. That closes the evaluator gap flagged in the module doc: mass predictions on the φ-ladder become genuine predictions rather than fitted torsion inputs.
Framework landmarks: T5 (J-uniqueness / RCL additive channels), T7 (eight-tick octave on $Q_3$), and T8 ($D=3$, three face-pair generation slots). The CW lower-set constraint and the variational ground-state zero together eliminate every competing coupling profile. Anyone auditing the mass formula yardstick $\cdot,\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$ needs this certificate to justify why generation gaps sit at 0, 11, and 17.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.