electron_rung
plain-language theorem explainer
Electron rung is fixed at the integer 2 as the baseline index on the phi-ladder for the first-generation lepton. Workers deriving lepton masses or proving the sector is geometry-derived cite this constant when unfolding the structural-mass expression. The declaration is a direct constant assignment with no reduction or tactic steps.
Claim. The electron rung is the integer $r_e := 2$, serving as the baseline rung index for the generation-1 lepton on the Recognition Science phi-ladder.
background
Recognition Science places lepton masses on a phi-ladder whose yardstick is scaled by powers of phi raised to (rung - 8). The electron rung is defined to equal 2 so that it matches the baseline generation-1 lepton. This module isolates the core electron-mass definitions to break import cycles within the T9 block.
proof idea
The declaration is a direct definition that assigns the integer 2.
why it matters
The value feeds the structural-mass definition m_struct = lepton_yardstick * phi^(r - 8) and the theorem lepton_sector_is_derived that shows all lepton constants follow from cube geometry. It supplies the rung anchor required by the eight-tick octave and the mass formula yardstick * phi^(rung - 8 + gap(Z)).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.