predicted_electron_mass

formal source

 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
 208    rw [← zpow_add₀ hne]; norm_num
 209  have h2 : phi ^ (57 : ℤ) * phi ^ (-6 : ℤ) = phi ^ (51 : ℤ) := by
 210    rw [← zpow_add₀ hne]; norm_num
 211  simp only [h1, mul_assoc]
 212  rw [h2]
 213
 214/-- Theorem: All lepton sector constants are derived from cube geometry.
 215    This proves the sector is parameter-free.