mass_ref_MeV
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the electron mass from the phi-ladder or cube geometry.
- Does not incorporate experimental uncertainty or error propagation.
- Does not apply to muon or tau masses.
- Does not replace the structural mass formula with an observed value.
Lean usage
noncomputable def residue : ℝ := Real.log (mass_ref_MeV / electron_structural_mass) / Real.log phiformal statement (Lean)
177def mass_ref_MeV : ℝ := 0.510998950
proof body
Definition body.
178
179/-- The Residue Δ = log_φ(m_obs / m_struct).
180 Value from audit: -20.70596. -/