`electron_structural_mass`

definition

show as: view math explainer →

module: IndisputableMonolith.RRF.Physics.ElectronMass.Defs
domain: RRF
line: 47 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.RRF.Physics.ElectronMass.Defs on GitHub at line 47.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  44  (2 : ℝ) ^ lepton_B * E_coh * phi ^ lepton_R0
  45
  46/-- The Structural Mass: m_struct = Y · φ^(r-8). -/
  47noncomputable def electron_structural_mass : ℝ :=
  48  lepton_yardstick * phi ^ (electron_rung - 8)
  49
  50/-- Dimensionless Structural Ratio to E_coh. -/
  51noncomputable def electron_structural_ratio : ℝ :=
  52  electron_structural_mass / E_coh
  53
  54/-! ## The Residue (The Break) -/
  55
  56/-- Observed Electron Mass (in MeV, placeholder for ratio matching).
  57    Ref: 0.510998950 MeV. -/
  58def mass_ref_MeV : ℝ := 0.510998950
  59
  60/-- The Residue Δ = log_φ(m_obs / m_struct).
  61    Value from audit: -20.70596. -/
  62noncomputable def electron_residue : ℝ :=
  63  Real.log (mass_ref_MeV / electron_structural_mass) / Real.log phi
  64
  65/-- The Electron Mass Formula (T9). -/
  66noncomputable def predicted_electron_mass : ℝ :=
  67  electron_structural_mass * phi ^ (gap 1332 - refined_shift)
  68
  69/-! ## Basic Theorem -/
  70
  71/-- Theorem: The Structural Mass is well-defined and forced by geometry.
  72
  73    m_struct = 2^(-22) * φ^(-5) * φ^62 * φ^(2-8)
  74             = 2^(-22) * φ^(62 - 5 + 2 - 8)
  75             = 2^(-22) * φ^51
  76
  77    Proof: Direct computation shows φ^(-5) * φ^62 * φ^(-6) = φ^51. -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.