lepton_sector_is_derived
plain-language theorem explainer
The lepton sector constants lepton_B and lepton_R0 are fixed by cube geometry at D=3 together with the sector count N_sec=2^(D-1) and the wallpaper count W=17. A researcher deriving parameter-free masses on the phi-ladder would cite this result to confirm the lepton sector carries no adjustable inputs. The proof is a one-line reflexivity that matches the left-hand sides to the geometric right-hand sides by definition.
Claim. $B_ {lepton} = - (ledger_bilateral_factor) · E_{passive}$ and $R_0^{lepton} = N_{sec} · W - (octave_period - electron_baseline_rung)$, where $N_{sec} = 2^{D-1}$, $E_{passive}$ is the passive edge count from the 3-cube, $W$ is the Fedorov wallpaper count, and the octave offset is taken from the generation-1 rung.
background
The module sets the lepton sector constants from cube geometry at D=3. Total edges equal 3·2²=12; one active edge per atomic tick leaves the passive count E_passive=11. N_sec is defined as 2^(D-1). The bilateral ledger factor supplies the doubling symmetry that appears in the binary exponent. lepton_B is therefore the negative product of that factor and E_passive. lepton_R0 is assembled as N_sec times the crystallographic count W=17 minus the octave adjustment from the electron baseline rung at 2. The local setting is the T9 derivation chain that treats all sector constants as forced by geometry rather than chosen by hand.
proof idea
The proof is a term-mode one-liner: exact ⟨rfl, rfl⟩. Reflexivity discharges both conjuncts once the definitions of lepton_B, lepton_R0, N_sec, ledger_bilateral_factor, E_passive, W, octave_period and electron_baseline_rung are unfolded.
why it matters
The theorem closes the lepton-sector derivation inside the T9 electron-mass module, showing every constant traces to D=3 (forced by the linking constraint) and to the eight-tick octave. It supports the claim that the electron mass rung on the phi-ladder is parameter-free. The result sits downstream of the cube-geometry and ledger-factorization structures and supplies the concrete values used in the mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.