`electron_structural_mass`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.ElectronMass.Defs on GitHub at line 161.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 158             lepton_B_eq, lepton_R0_eq]
 159
 160/-- The Structural Mass: m_struct = Y · φ^(r-8). -/
 161noncomputable def electron_structural_mass : ℝ :=
 162  lepton_yardstick * phi ^ (electron_rung - (octave_period : ℤ))
 163
 164/-- Dimensionless Structural Ratio to E_coh. -/
 165noncomputable def electron_structural_ratio : ℝ :=
 166  electron_structural_mass / E_coh
 167
 168/-! ## The Residue (The Break) -/
 169
 170/-- Observed Electron Mass (in MeV, placeholder for ratio matching).
 171    Ref: 0.510998950 MeV.
 172
 173    IMPORTANT: “MeV” here is a **display convention** used for PDG comparisons.
 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

papers checked against this theorem

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