mass_ref_MeV

formal source

 174    The RS-native core is dimensionless; any SI/eV/MeV reporting must be treated
 175    as an explicit calibration seam. This value is used only for the *diagnostic*
 176    extracted residue `electron_residue`, not for the forward mass prediction. -/
 177def mass_ref_MeV : ℝ := 0.510998950
 178
 179/-- The Residue Δ = log_φ(m_obs / m_struct).
 180    Value from audit: -20.70596. -/
 181noncomputable def electron_residue : ℝ :=
 182  Real.log (mass_ref_MeV / electron_structural_mass) / Real.log phi
 183
 184/-- The Electron Mass Formula (T9). -/
 185noncomputable def predicted_electron_mass : ℝ :=
 186  electron_structural_mass * phi ^ (gap 1332 - refined_shift)
 187
 188/-! ## Main Theorems -/
 189
 190/-- Theorem: The Structural Mass is well-defined and forced by geometry.
 191
 192    m_struct = 2^(-22) * φ^(-5) * φ^62 * φ^(2-8)
 193             = 2^(-22) * φ^(62 - 5 + 2 - 8)
 194             = 2^(-22) * φ^51
 195
 196    Proof: Direct computation shows φ^(-5) * φ^62 * φ^(-6) = φ^51. -/
 197theorem electron_structural_mass_forced :
 198    electron_structural_mass = (2 : ℝ) ^ (-22 : ℤ) * phi ^ (51 : ℤ) := by
 199  unfold electron_structural_mass lepton_yardstick
 200  rw [E_coh_eq]
 201  simp only [lepton_B_eq, lepton_R0_eq, electron_rung_eq, octave_period_eq]
 202  have hne : (phi : ℝ) ≠ 0 := phi_ne_zero
 203  -- Simplify 2 - 8 to -6
 204  have hsub : (2 : ℤ) - (8 : ℕ) = (-6 : ℤ) := by norm_num
 205  simp only [hsub]
 206  -- Now combine the phi powers
 207  have h1 : phi ^ (-5 : ℤ) * phi ^ (62 : ℤ) = phi ^ (57 : ℤ) := by