lepton_residues_distinct
plain-language theorem explainer
The three lepton generations occupy distinct residue classes modulo 8 under the RS rung map. A physicist deriving forced mass hierarchies from geometric constraints would cite this to confirm ladder stability. The proof reduces directly to unfolding the rung definitions via simplification.
Claim. The rung assignments satisfy $(r_e mod 8) neq (r_mu mod 8)$, $(r_mu mod 8) neq (r_tau mod 8)$, and $(r_e mod 8) neq (r_tau mod 8)$, where each $r_f$ is the integer rung position assigned to fermion $f$ in the Recognition Science bridge.
background
In Recognition Science the lepton ladder is built from the electron structural mass (T9) together with step functions drawn from cubic voxel geometry and the golden ratio. The rung function places each generation at a discrete position on the phi-ladder; the eight-tick octave induces a natural Z_8 torsion group on these positions. Distinct residues are required for topological stability, with transitions controlled by passive edge count 11 and face count 6.
proof idea
The proof is a direct term-mode verification. Constructor splits the conjunction into three inequalities; each is discharged by simp on the RSBridge.rung definition, which reduces the modular comparisons to explicit numerical checks on the assigned rungs for electron, muon, and tau.
why it matters
This theorem is invoked by lepton_torsion_verified to certify the full torsion stability constraint. It supplies the distinct-residue half of the T10 necessity argument, showing that the lepton masses are forced once the electron mass and cube-derived constants are fixed, consistent with the eight-tick structure and phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.