fermionRung
plain-language theorem explainer
fermionRung maps each Standard Model fermion to its integer rung on the phi-ladder for use in the mass formula. Researchers verifying Recognition Science predictions against PDG data cite this mapping when assembling theoretical masses for leptons and quarks. The definition is an exhaustive pattern match on the Fermion inductive type that delegates directly to the rung functions r_lepton, r_up, and r_down.
Claim. The function $r :$ Fermion $→ ℤ$ sends electron to 2, muon to 13, tauon to 19, up to 4, charm to 15, top to 21, down to 4, strange to 15, and bottom to 21, where the increments for second and third generations are supplied by the torsion values $τ(1)=11$ and $τ(2)=17$.
background
The Recognition Science mass law states $m(particle) = $ yardstick(Sector) $× φ^{r-8 + gap(Z)}$, with $r$ the rung integer on the phi-ladder. The Fermion inductive type enumerates the nine charged leptons and quarks. Upstream definitions supply the concrete rung values: r_lepton starts leptons at baseline 2 and adds τ(generation), r_up and r_down start quarks at 4 and add the same torsion, while τ itself is defined as 0, 11, or 17 according to generation.
proof idea
Pattern-matching definition on the nine Fermion constructors. Each case calls the appropriate upstream rung function (r_lepton for leptons, r_up for up-type quarks, r_down for down-type quarks) with the particle label string; the rung functions themselves are direct case distinctions on the torsion values.
why it matters
fermionRung supplies the rung parameter required by fermionMass, which assembles the full predicted mass for every fermion via predict_mass. This completes the formal RS mass statements for the Standard Model inside the module that compares them to PDG 2024 values. It instantiates the phi-ladder forced by T6 and the eight-tick octave of T7 within the D=3 geometry that fixes the yardstick.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.