sectorBaseRung
plain-language theorem explainer
Base rung values on the phi-ladder are assigned to fermion sectors by charge structure Z: 2 for leptons and 4 for both up and down quark sectors. Researchers deriving particle masses from generation torsion in Recognition Science cite this when populating the RSLedger for rung-based mass formulas. The definition uses direct case distinction on the three constructors of FermionSector.
Claim. Define the base rung map $b$ from fermion sectors to integers by $b($leptons$)=2$, $b($up-quarks$)=4$, and $b($down-quarks$)=4$.
background
The RSLedger structure augments a minimal ledger with generation torsion offsets and sector base rungs to support mass derivation on the phi-ladder. FermionSector is the inductive type with constructors leptons, upQuarks, and downQuarks. Generation is the inductive type with first, second, and third. Module documentation states that particle masses occupy discrete rungs with full rung = baseRung + torsion, so mass ratios equal phi to the rung difference. Torsion values 0, 11, 17 arise from D=3 cube combinatorics.
proof idea
The definition is given directly by pattern matching on the three constructors of FermionSector, returning the constants 2, 4, and 4. No lemmas are invoked; it encodes the charge-derived base values as a simple case split.
why it matters
This supplies the baseRung field to canonicalRSLedger, which pairs it with generationTorsion to assemble the complete ledger. It realizes the rung assignment rung = baseRung + tau_g that yields mass ratios m_f / m_g = phi^{r_f - r_g} in the Recognition Science framework. The values connect to the phi-ladder and the geometric torsion derivation from the D=3 cube.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.