electron_structural_ratio

formal source

 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
 192    m_struct = 2^(-22) * φ^(-5) * φ^62 * φ^(2-8)
 193             = 2^(-22) * φ^(62 - 5 + 2 - 8)
 194             = 2^(-22) * φ^51
 195