LeptonTorsionCert
plain-language theorem explainer
LeptonTorsionCert packages the forced rung assignments for the electron, muon, and tau together with residue distinctness modulo 8 and stability of the ladder. Physicists working on mass hierarchies in Recognition Science would cite this certificate when verifying that the lepton spectrum follows from the eight-tick structure and cube geometry. The definition is a direct packaging of the rung values 2, 13, 19 with the stability predicate.
Claim. The certificate asserts that the Recognition Science rung function satisfies $r(e)=2$, $r(mu)=13$, $r(tau)=19$, that these values are pairwise incongruent modulo 8, and that the sequence 2,13,19 forms a stable lepton ladder under the is_stable_lepton_ladder predicate.
background
In the Recognition Science framework the lepton generations sit on the phi-ladder via the RSBridge.rung map, which assigns the electron rung 2, the muon rung 13 and the tau rung 19. Module T10 replaces the two lepton axioms of LeptonGenerations.lean by proving these rungs are forced from the electron structural mass (T9), the step functions E_passive=11 and W=17 drawn from cube geometry, and the golden ratio phi. The predicate is_stable_lepton_ladder 2 13 19 encodes the stability condition required by the mass formula yardstick * phi^(rung-8+gap(Z)). Upstream results supply the explicit rung table in RSBridge and the generation torsion tau(gen) that yields 0,11,17.
proof idea
This is a structure definition that directly assembles the three properties: the forced equalities are taken verbatim from the RSBridge.rung table, the distinct-residues clause follows by direct computation of the values modulo 8, and the stable field is supplied by the sibling lemma is_stable_lepton_ladder.
why it matters
LeptonTorsionCert is the packaging object consumed by the downstream theorem lepton_torsion_verified, which constructs an explicit instance to certify that the lepton ladder is forced. It closes the T10 necessity step that derives the muon and tau masses from T9 and the geometric constants (cube faces, wallpaper groups, alpha band) already obtained from the eight-tick octave. The rungs 2,13,19 arise by adding the torsion increments 0,11,17 to the base electron rung, completing the mass-hierarchy derivation for the lepton sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.