rung
plain-language theorem explainer
The rung function assigns an integer level on the phi-ladder to a named particle within one of four sectors. Mass and energy modelers cite it to anchor predictions via the yardstick times phi to the power of rung. The implementation selects the sector-specific table by pattern matching on the sector constructor.
Claim. $r(s,n)$ equals the integer from the lepton table when $s$ is the lepton sector, from the up-quark table when $s$ is the up-quark sector, from the down-quark table when $s$ is the down-quark sector, or from the boson table when $s$ is the electroweak sector.
background
The masses domain anchors particle masses to the phi-ladder via the formula yardstick times phi to the power of (rung minus 8 plus gap). The Sector type classifies particles into lepton, up-quark, down-quark, and electroweak families. Upstream tables in Anchor fix the integers: leptons give electron rung 2, muon 13, tau 19; down quarks give d rung 4, s 15, b 21; up quarks and bosons receive parallel assignments.
proof idea
The definition performs case analysis on the sector constructor and delegates directly to the corresponding pre-defined integer map for that family.
why it matters
This declaration supplies the rung input to downstream results including hearingLossPenalty_zero, GeometricStrain, E_base_pos, E_PBM_bounds, and settlementLevelCount_eq. It realizes the rung component of the mass formula on the phi-ladder, linking to the J-uniqueness property and the self-similar fixed point in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.