electron_baseline_rung
plain-language theorem explainer
The electron baseline rung fixes the lowest lepton generation at integer value 2 on the phi-ladder. Mass derivations in the lepton sector cite this constant to anchor the electron scale before computing R0 and coherence exponents. The declaration is a direct assignment of 2, taken from the active-edges-per-tick count plus one.
Claim. The baseline rung for the electron lepton is the integer 2.
background
In the T9 Electron Mass Definitions module, lepton constants arise from D = 3 cube geometry. Cube edges total 12, one active edge per tick leaves 11 passive edges, and wallpaper groups supply the factor 17. The octave period equals 8 ticks from the eight-tick structure. The baseline rung equals active edges per tick plus one, fixing the electron at the lowest generation on the phi-ladder.
proof idea
This is a direct definition that assigns the integer 2. It matches the upstream count of active edges per tick plus one, with no further reduction required.
why it matters
The definition supplies the starting rung for lepton_R0 and the theorem that the lepton sector is parameter-free. It realizes the chain step from D = 3 and the eight-tick octave, ensuring the electron mass formula begins at the correct phi-exponent without free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.