electron_rung
plain-language theorem explainer
The definition assigns the electron rung the integer value 2 on the phi-ladder. Researchers deriving lepton masses from cube geometry and the eight-tick octave cite it as the baseline for the first-generation lepton. It is a direct alias to the baseline rung obtained from active edges per tick plus one.
Claim. The electron rung is the integer $r_e = 2$, the baseline value for the first-generation lepton on the phi-ladder.
background
This module supplies the core definitions for the electron mass derivation under T9. It separates definitions from theorems to avoid import cycles and shows that lepton constants follow from D = 3 cube geometry: 12 total edges, one active edge per tick, 11 passive edges, and 17 wallpaper groups. The rung enters the mass formula as the exponent offset from the octave period of 8. Upstream, electron_baseline_rung is defined as 2, obtained directly as active_edges_per_tick + 1, and the sibling RRF module repeats the same assignment.
proof idea
One-line definition that aliases electron_baseline_rung.
why it matters
This supplies the rung value required by electron_structural_mass and lepton_sector_is_derived. The latter proves all lepton constants are forced by cube geometry, N_sec = 4, W = 17, and the octave offset, confirming the sector is parameter-free. It anchors the mass formula yardstick * phi^(rung - 8) at the electron scale and links to the T7 eight-tick period and T8 D = 3 forcing steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.