torsion_minimality_forced
plain-language theorem explainer
Any integer triple satisfying the stable lepton ladder predicate must have rung differences exactly 11 and 6. Physicists constructing lepton mass hierarchies from Recognition Science geometry cite this to lock the generational steps once the electron mass is fixed. The proof is a direct unfolding of the stability definition followed by simplification against the 3-cube edge and face counts.
Claim. For all integers $r_1,r_2,r_3$, if $r_1,r_2,r_3$ satisfy the torsion stability conditions (distinct residues modulo 8 together with rung transitions matching the passive edge count of the 3-cube and its face count), then $r_2-r_1=11$ and $r_3-r_2=6$.
background
The module T10 proves that the muon and tau masses are forced once the electron mass (T9) and the geometric constants from cube geometry are given. The predicate is_stable_lepton_ladder requires three integers to occupy distinct residue classes modulo 8 and to obey rung transitions fixed by the cubic voxel: the first step equals the passive edge count E_passive = cube_edges(3) - 1 and the second step equals the face count cube_faces(3). Upstream, cube_edges(d) is defined as d * 2^(d-1) and cube_faces(d) as 2d; for d=3 these evaluate to 12 and 6 respectively, so the passive count is 11.
proof idea
The term proof introduces the three integers and the stability hypothesis, unfolds is_stable_lepton_ladder to expose the two step equalities, performs rcases to isolate them, then applies simpa with the cube_edges and cube_faces definitions to reduce the expressions to the numerals 11 and 6.
why it matters
The declaration supplies the concrete numerical steps required by the lepton ladder in the Necessity module, replacing earlier axioms with derived constants. It sits downstream of the cube geometry results in AlphaDerivation and MassTopology and supports the T10 claim that the full lepton spectrum is fixed by the eight-tick structure and D=3. No open scaffolding remains for this particular extraction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.