Masses Verification Muon Electron Ratio Error

The muon-electron ratio check

The muon and electron are two of the three charged leptons, the family of lightweight particles that includes the electron, the muon, and the tau. Their measured masses are 105.6583755 MeV and 0.51099895069 MeV respectively, so the muon is about 206.77 times heavier than the electron. That ratio is a pure number, free of units, and it is the quantity the Recognition Science declaration muon_electron_ratio_error examines.

Recognition Science is a framework that starts from a single assumption: reality keeps a discrete record of recognition events, and the cost of recognition is forced, not chosen. From that assumption, the framework's machine-checked library of formal theorems derives a mass ladder: particle masses sit on a phi-power ladder, where phi is the golden ratio, approximately 1.618. For the lepton sector, the framework's prediction for the muon-electron mass ratio is phi raised to the power 11.

The declaration establishes a precise numerical fact. It proves that the measured muon-electron ratio lies strictly between 206.76 and 206.77. It also proves that the golden-ratio prediction, phi^11, is strictly less than that measured ratio. In other words, the framework's predicted ratio undershoots the measured value. The declaration does not claim the prediction matches the measurement to any particular precision; it only establishes the direction and rough size of the gap.

The declaration also proves a separate fact about the tau-electron ratio: the measured value lies strictly between 3477 and 3478, and the golden-ratio prediction phi^17 is strictly greater than that measured value. So for the tau, the prediction overshoots. These two results together show that the phi-power ladder places the lepton mass ratios in the right neighborhood, but not exactly on the measured values.

What the declaration does not claim is as important as what it proves. The experimental masses are imported constants, not derived from the framework. The framework's own documentation marks this comparison as quarantined from the certified surface: the measured values are taken from the Particle Data Group's 2024 review, and the comparison is an empirical check, not a theorem. The declaration proves inequalities about ratios of those imported constants, but it does not prove that the masses themselves follow from the framework's axioms.

The practical consequence is a clear picture of where the framework stands. The phi-power ladder gets the lepton mass ratios within a few percent, with the muon ratio undershooting and the tau ratio overshooting. That is a genuine, machine-checked result about the framework's predictive power, and it is honestly bounded: the framework does not derive the masses, it only places their ratios near the measured values.

theorem ratio_mu_e_exp_bounds :
    (206.76 : ℝ) < ratio_mu_e_exp ∧ ratio_mu_e_exp < (206.77 : ℝ) := by
  unfold ratio_mu_e_exp m_mu_exp m_e_exp; constructor <;> norm_num

theorem muon_ratio_undershoot :
    Constants.phi ^ (11 : ℕ) < ratio_mu_e_exp := by
  linarith [phi11_lt, ratio_mu_e_exp_bounds.1]

theorem tau_ratio_overshoot :
    ratio_tau_e_exp < Constants.phi ^ (17 : ℕ) := by
  linarith [phi17_gt, ratio_tau_e_exp_bounds.2]

theorem ratio_tau_e_exp_bounds :
    (3477 : ℝ) < ratio_tau_e_exp ∧ ratio_tau_e_exp < (3478 : ℝ) := by
  unfold ratio_tau_e_exp m_tau_exp m_e_exp; constructor <;> norm_num

def m_mu_exp : ℝ := 105.6583755

def m_e_exp : ℝ := 0.51099895069

What this page does not claim

The declaration does not claim the muon-electron ratio prediction matches the measured value to any stated precision. The declaration does not claim the experimental masses are derived from the framework's axioms. The declaration does not claim the framework predicts the absolute scale of lepton masses, only the ratios.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Masses/Verification.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: