electron_rung_eq
plain-language theorem explainer
Recognition Science fixes the electron rung at 2 as the baseline for generation-1 leptons on the phi-ladder. Mass derivations cite this equality when simplifying structural mass expressions that combine yardstick, B exponent, and R0 offset. The proof is a direct reflexivity reduction after the definition of electron_rung unfolds to the baseline value.
Claim. The baseline rung $r_e$ for the electron satisfies $r_e = 2$.
background
The T9 module derives lepton constants from D = 3 cube geometry yielding 12 edges, one active per tick, and 11 passive edges. This produces B_pow(Lepton) = -22 and r0(Lepton) = 62 via 17 wallpaper groups and the octave offset from rung 2. Electron rung is defined as the baseline rung, the lowest phi-exponent compatible with ledger closure at the electron scale. Upstream structures include SpectralEmergence forcing three generations from face-pair count and PhiForcingDerived establishing J-cost convexity with unique minimum at x = 1.
proof idea
The proof is a one-line term-mode reflexivity. It reduces the equality directly via the definition of electron_rung as electron_baseline_rung, which evaluates to 2.
why it matters
This equality is invoked in electron_structural_mass_forced to reduce the mass expression to 2^{-22} phi^{51}. It closes the T9 chain linking D = 3, passive edge count 11, wallpaper groups 17, and the eight-tick octave to concrete lepton masses. The module documentation states that these constants are forced by geometry rather than free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.