mass_ref_MeV
plain-language theorem explainer
mass_ref_MeV supplies the fixed reference 0.510998950 MeV for the observed electron mass, serving as calibration input for residue extraction in the lepton sector. Researchers comparing phi-ladder structural predictions to PDG data cite this constant when computing the diagnostic defect. The definition is a direct real-number assignment with no further computation.
Claim. The reference electron mass is defined as $0.510998950$ MeV and used solely to calibrate the residue $Δ = log_φ(m_obs / m_struct)$.
background
The module isolates T9 electron mass definitions from theorems to break import cycles. It derives lepton constants from D = 3 via cube geometry: 12 total edges, one active transition per tick, and 11 passive field edges that fix the binary exponent at -22. The baseline rung r_e = 2 follows from the 8-tick octave offset and 17 wallpaper groups. Upstream, PrimitiveDistinction.from reduces seven axioms to four structural conditions plus three definitional facts that ground these constants.
proof idea
The definition is a direct constant assignment of the real value 0.510998950.
why it matters
This constant anchors the electron_residue definition that implements the T9 mass formula. It supplies the observed input for the residue that connects to the structural mass on the phi-ladder. The placement ties the diagnostic directly to framework steps T8 (D = 3) and T7 (eight-tick octave) while feeding both the main and RRF electron_residue sites.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.