is_stable_lepton_ladder
plain-language theorem explainer
The torsion stability constraint requires three lepton rung indices to occupy distinct classes modulo 8, with consecutive differences fixed at 11 and 6, and the lowest rung anchored at 2. Physicists deriving forced lepton mass hierarchies from cubic geometry would cite this predicate to justify the uniqueness of the electron-muon-tau configuration. The definition assembles the conditions as a direct conjunction of residue and step predicates taken from the hypercube edge and face counts.
Claim. A triple of integers $(r_1, r_2, r_3)$ satisfies the lepton torsion stability condition when $r_1 = 2$, $r_2 - r_1 = 11$, $r_3 - r_2 = 6$, and the three values are pairwise incongruent modulo 8.
background
The module T10 Necessity establishes that the lepton ladder is forced once the electron mass (T9) and the geometric constants from the cubic voxel are given. The functions cube_edges(d) = d * 2^{d-1} and cube_faces(d) = 2d supply the step sizes: for d = 3 the first transition is the passive edge count minus one (11) and the second is the face count (6). These arise from the eight-tick octave (T7) that induces a Z_8 torsion group on rung indices, together with the D = 3 spatial dimensions fixed by the forcing chain. Upstream results include the cube-edge and cube-face definitions in AlphaDerivation and the inductive Lepton type in CubeFaceUniversality.
proof idea
The definition is a direct conjunction of four arithmetic conditions: pairwise incongruence of the rungs modulo 8, the first difference equal to cube_edges(3) - 1, the second difference equal to cube_faces(3), and the base rung fixed at 2. No lemmas are applied; the body simply unfolds the geometric constants already derived in the imported AlphaDerivation module.
why it matters
This predicate supplies the stability criterion used to prove uniqueness of the rung set {2, 13, 19} in lepton_rungs_unique and to construct the LeptonTorsionCert structure. It closes part of the T10 necessity argument by encoding the geometric forcing from the cubic ledger and the eight-tick octave (T7), ensuring the muon and tau masses are determined once the electron mass is fixed. It touches the open question of whether higher generations remain stable under the full Recognition Field dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.