rung
plain-language theorem explainer
The rung assignment maps each of the twelve Standard Model fermions to a fixed integer on the phi-ladder. Researchers computing masses via the yardstick times phi to the power of (rung minus 8 plus gap of Z) would cite these tabulated values when applying the mass formula. The definition is implemented as exhaustive case analysis on the Fermion inductive type.
Claim. Let $F$ be the set of twelve Standard Model fermions. The function $r: F → ℤ$ is given by the table $r(e)=2$, $r(μ)=13$, $r(τ)=19$, $r(u)=4$, $r(c)=15$, $r(t)=21$, $r(d)=4$, $r(s)=15$, $r(b)=21$, $r(ν₁)=0$, $r(ν₂)=11$, $r(ν₃)=19$.
background
The module supplies the bridge from the recognition framework to particle physics. It introduces the Fermion inductive type with twelve constructors for the six quarks, three charged leptons and three neutrinos. The gap function is the closed-form display $F(Z) = ln(1 + Z/φ)/ln(φ)$, and the mass-at-anchor formula uses the yardstick scaled by φ raised to (rung − 8 + gap(ZOf i)). The local theoretical setting is Single Anchor Phenomenology, where the integrated RG residue at the anchor scale equals the gap value with tolerance ~1e-6.
proof idea
The definition is a direct case analysis that matches each of the twelve Fermion constructors and returns the corresponding integer constant.
why it matters
This supplies the rung indices that feed the mass formula used by forty downstream declarations, including E_base_pos and E_PBM_bounds in PhotobiomodulationDevice and hearingLossPenalty_zero in Acoustics. It realizes the phi-ladder step in the T5–T8 forcing chain, where phi is forced as the self-similar fixed point and the eight-tick octave appears. The assignment connects to the Recognition Composition Law through J-cost evaluations in applied modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.