lepton_R0
plain-language theorem explainer
The declaration defines the lepton sector geometric origin R0 as the integer 62 for the Recognition Science electron mass derivation. Researchers assembling the yardstick scale from the phi-ladder cite this constant when reducing structural masses. It enters as a direct constant definition to separate from theorems and avoid import cycles in the T9 module.
Claim. The lepton sector geometric origin parameter $R_0$ equals the integer 62.
background
The T9 Electron Mass Definitions module isolates core constants for the electron mass to break import cycles. lepton_R0 encodes the geometric origin for the lepton sector on the phi-ladder. Upstream results define it via the formula R0 = N_sec * W - (octave_period - electron_baseline_rung), where N_sec = 4 from D = 3 spatial dimensions, W = 17 from wallpaper groups, octave_period = 8, and baseline rung = 2, which evaluates to 62. This constant combines with E_coh = phi^{-5} and the bilateral factor B to form the yardstick Y = 2^B * E_coh * phi^{R0}.
proof idea
This declaration is a direct definition that assigns the integer 62. It serves as the constant value referenced by the sibling theorem lepton_R0_eq, which proves equality via simplification and numerical normalization on the expanded expression from MassTopology.
why it matters
This definition provides the R0 input required by lepton_yardstick and electron_structural_mass_forced, where the latter reduces the structural mass to 2^{-22} * phi^{51}. It completes a step in the T9 electron mass definitions, linking the lepton sector to the eight-tick octave and three-dimensional geometry from the forcing chain T0-T8. The value remains fixed once the wallpaper groups and sector count are accepted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.