lepton_R0
plain-language theorem explainer
The lepton sector geometric origin R0 is defined by the arithmetic expression N_sec times W minus the difference between the octave period and the electron baseline rung. Researchers deriving the electron mass from cube geometry in Recognition Science would cite this to anchor the phi-exponent for the lepton yardstick. The definition directly substitutes the constants N_sec = 4, W = 17, octave_period = 8, and electron_baseline_rung = 2 to yield the integer 62.
Claim. $R_0 := N_{sec} · W - (octave period - r_{baseline})$, where $N_{sec} = 2^{D-1}$ is the number of fermion sectors at spatial dimension $D=3$, $W=17$ is the number of wallpaper groups, the octave period equals 8, and $r_{baseline}=2$.
background
In the T9 Electron Mass Definitions module the lepton sector constants are derived from the geometry of the 3-cube and the 17 wallpaper groups. N_sec is defined as 2^(D-1)=4 at D=3, representing the number of fermion sectors. The octave_period is 2^D=8 from the eight-tick period in T6. The electron_baseline_rung is set to 2 as the lowest lepton generation from active edges plus one. The wallpaper groups W=17 enter as an external mathematical fact from crystallographic classification. This definition computes the rung offset R0 for the phi-ladder in the lepton sector.
proof idea
This is a direct definition that substitutes the referenced constants N_sec, MassTopology.W, octave_period, and electron_baseline_rung. No tactics are applied; the body is a single arithmetic expression. The downstream theorem lepton_R0_eq confirms the evaluation to 62 by simplification and norm_num.
why it matters
This definition supplies the geometric origin for the lepton sector rung R0=62, which is used in lepton_yardstick to set the scale Y = 2^B * E_coh * phi^R0. It feeds the theorem lepton_sector_is_derived proving all lepton constants are derived from cube geometry, and ultimately the structural mass formula m_struct = 2^(-22) * phi^51 in electron_structural_mass_forced. It realizes the T9 step linking D=3, the 11 passive edges, and the 17 wallpaper groups to fix the phi-exponent without free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.