Encyclopedia Verification Verification Mass Comparison

ARTICLE 4 claims 2 theorems 2 measured

Verification Mass Comparison

A machine-checked module compares predicted particle masses against 2024 experimental values, showing where the framework's golden-ratio ladder lands.

Verify this page

Checking masses against measurement

Verification mass comparison is the practice of taking a theoretical prediction and holding it next to a measured number. In Recognition Science, the prediction comes from a formula that ties every particle's mass to powers of the golden ratio, phi, roughly 1.618. The measured numbers come from the Particle Data Group's 2024 review, the standard world summary of experimental particle physics. The module that performs this comparison is a machine-checked library of formal theorems, meaning every step of the arithmetic is verified by a computer, not asserted by hand.

The mass formula works like this. Each family of particles, such as leptons or quarks, has a yardstick set by its sector. That yardstick is multiplied by phi raised to an integer rung. For example, the electron sits on rung 2, the muon on rung 13, and the tau on rung 19. The ratio of the muon mass to the electron mass is therefore phi to the power 11, and the ratio of the tau to the electron is phi to the power 17. The module proves these rung assignments are derived, not guessed, and it proves bounds on the resulting ratios: phi to the 11th power lies between 198.9 and 200, and phi to the 17th power lies between 3500 and 3600.

What does the comparison actually show? The measured ratio of the muon mass to the electron mass is between 206 and 207. The measured ratio of the tau mass to the electron mass is between 3477 and 3478. The phi-based predictions land close: 198.9 to 200 for the muon, 3500 to 3600 for the tau. The agreement is not exact, and the module is honest about that. It is quarantined from the framework's certified surface precisely because it imports experimental values and depends on an anchor system. The comparison is an empirical check, not a theorem about nature.

The module also records the measured masses themselves, with uncertainties, for the electron, muon, tau, the five quarks, and the W, Z, and Higgs bosons. These are stored as plain definitions, not derived results. The point of the module is to make the check reproducible: anyone can run the same arithmetic and see where the golden-ratio ladder matches the world and where it does not. That is what verification mass comparison establishes in plain language: a precise, auditable statement of how far the framework's predictions reach, and where they fall short.

THEOREM lepton_rungs_derived · ratio_mu_e_RS · ratio_tau_e_RS · IndisputableMonolith/Verification/MassComparison.lean
lepton_rungs_derived · IndisputableMonolith/Verification/MassComparison.lean:123 
/-- Lepton rung integers (derived from generation structure). -/
theorem lepton_rungs_derived :
    r_lepton "e" = 2 ∧ r_lepton "mu" = 13 ∧ r_lepton "tau" = 19 := r_lepton_values
ratio_mu_e_RS · IndisputableMonolith/Verification/MassComparison.lean:138 
/-- Predicted m_μ / m_e ratio (using rung integers). -/
noncomputable def ratio_mu_e_RS : ℝ := phi ^ (r_lepton "mu" - r_lepton "e")
ratio_tau_e_RS · IndisputableMonolith/Verification/MassComparison.lean:151 
/-- Predicted m_τ / m_e ratio (using rung integers). -/
noncomputable def ratio_tau_e_RS : ℝ := phi ^ (r_lepton "tau" - r_lepton "e")
THEOREM phi_pow_11_approx · phi_pow_17_approx · IndisputableMonolith/Verification/MassComparison.lean
phi_pow_11_approx · IndisputableMonolith/Verification/MassComparison.lean:171 
/-- φ^11 is approximately 199.005... (proven coarse bounds).
    Derived from certified bounds on φ, φ³, and φ⁸ in `Numerics.Interval.PhiBounds`. -/
theorem phi_pow_11_approx : (198.9 : ℝ) < phi ^ (11 : ℕ) ∧ phi ^ (11 : ℕ) < (200 : ℝ) := by
  -- Import certified bounds on `Real.goldenRatio` and translate them to `Constants.phi`.
  have h8_lo : (46.97 : ℝ) < phi ^ (8 : ℕ) := by
    simpa [Constants.phi, Real.goldenRatio] using
      (IndisputableMonolith.Numerics.phi_pow8_gt)
  have h8_hi : phi ^ (8 : ℕ) < (46.99 : ℝ) := by
    simpa [Constants.phi, Real.goldenRatio] using
      (IndisputableMonolith.Numerics.phi_pow8_lt)
  have h3_lo : (4.236 : ℝ) < phi ^ (3 : ℕ) := by
    simpa [Constants.phi, Real.goldenRatio] using
      (IndisputableMonolith.Numerics.phi_cubed_gt)
  have h3_hi : phi ^ (3 : ℕ) < (4.237 : ℝ) := by
    simpa [Constants.phi, Real.goldenRatio] using
      (IndisputableMonolith.Numerics.phi_cubed_lt)
  have hpow : phi ^ (11 : ℕ) = phi ^ (8 : ℕ) * phi ^ (3 : ℕ) := by
    have h : (8 + 3 : ℕ) = 11 := by norm_num
    simpa [h, pow_add] using (pow_add phi 8 3)
  constructor
  · -- Lower bound
    have hmul :
        (46.97 : ℝ) * (4.236 : ℝ) < (phi ^ (8 : ℕ)) * (phi ^ (3 : ℕ)) := by
      have hpos4236 : (0 : ℝ) < (4.236 : ℝ) := by norm_num
      have hpos8 : (0 : ℝ) < phi ^ (8 : ℕ) := by
        have hφ : 0 < phi := Constants.phi_pos
        exact pow_pos hφ _
      have h1 :
          (46.97 : ℝ) * (4.236 : ℝ) < (phi ^ (8 : ℕ)) * (4.236 : ℝ) :=
        mul_lt_mul_of_pos_right h8_lo hpos4236
      have h2 :
          (phi ^ (8 : ℕ)) * (4.236 : ℝ) < (phi ^ (8 : ℕ)) * (phi ^ (3 : ℕ)) :=
        mul_lt_mul_of_pos_left h3_lo hpos8
      exact lt_trans h1 h2
    have h1989 : (198.9 : ℝ) < (46.97 : ℝ) * (4.236 : ℝ) := by norm_num
    have hmul' : (46.97 : ℝ) * (4.236 : ℝ) < phi ^ (11 : ℕ) := by
      simpa [hpow] using hmul
    exact lt_trans h1989 hmul'
  · -- Upper bound
    have hmul :
        (phi ^ (8 : ℕ)) * (phi ^ (3 : ℕ)) < (46.99 : ℝ) * (4.237 : ℝ) := by
      have hpos3 : (0 : ℝ) < phi ^ (3 : ℕ) := by
        have hφ : 0 < phi := Constants.phi_pos
        exact pow_pos hφ _
      have hpos4699 : (0 : ℝ) < (46.99 : ℝ) := by norm_num
      have h1 :
          (phi ^ (8 : ℕ)) * (phi ^ (3 : ℕ)) < (46.99 : ℝ) * (phi ^ (3 : ℕ)) :=
        mul_lt_mul_of_pos_right h8_hi hpos3
      have h2 :
          (46.99 : ℝ) * (phi ^ (3 : ℕ)) < (46.99 : ℝ) * (4.237 : ℝ) :=
        mul_lt_mul_of_pos_left h3_hi hpos4699
      exact lt_trans h1 h2
    have h200 : (46.99 : ℝ) * (4.237 : ℝ) < (200 : ℝ) := by norm_num
    have hmul' : phi ^ (11 : ℕ) < (46.99 : ℝ) * (4.237 : ℝ) := by
      simpa [hpow] using hmul
    exact lt_trans hmul' h200
phi_pow_17_approx · IndisputableMonolith/Verification/MassComparison.lean:228 
/-- φ^17 is approximately 3571.0... (proven coarse bounds).
    This is sufficient to certify the *sign* of the raw τ/e discrepancy. -/
theorem phi_pow_17_approx : (3500 : ℝ) < phi ^ (17 : ℕ) ∧ phi ^ (17 : ℕ) < (3600 : ℝ) := by
  have h8_lo : (46.97 : ℝ) < phi ^ (8 : ℕ) := by
    simpa [Constants.phi, Real.goldenRatio] using
      (IndisputableMonolith.Numerics.phi_pow8_gt)
  have h8_hi : phi ^ (8 : ℕ) < (46.99 : ℝ) := by
    simpa [Constants.phi, Real.goldenRatio] using
      (IndisputableMonolith.Numerics.phi_pow8_lt)
  have hφ_lo : (1.618 : ℝ) < phi := by
    simpa [Constants.phi, Real.goldenRatio] using
      (IndisputableMonolith.Numerics.phi_gt_1618)
  have hφ_hi : phi < (1.6185 : ℝ) := by
    simpa [Constants.phi, Real.goldenRatio] using
      (IndisputableMonolith.Numerics.phi_lt_16185)
  have hpow16 : phi ^ (16 : ℕ) = (phi ^ (8 : ℕ)) * (phi ^ (8 : ℕ)) := by
    have h : (8 + 8 : ℕ) = 16 := by norm_num
    simpa [h, pow_add] using (pow_add phi 8 8)
  have hpow17 : phi ^ (17 : ℕ) = (phi ^ (16 : ℕ)) * phi := by
    have h : (16 + 1 : ℕ) = 17 := by norm_num
    simpa [h, pow_add] using (pow_add phi 16 1)
  constructor
  · -- Lower bound
    have h16_mul :
        (46.97 : ℝ) * (46.97 : ℝ) < (phi ^ (8 : ℕ)) * (phi ^ (8 : ℕ)) := by
      have hpos8 : 0 < phi ^ (8 : ℕ) := by
        have hφ : 0 < phi := Constants.phi_pos
        exact pow_pos hφ _
      have hpos4697 : (0 : ℝ) < (46.97 : ℝ) := by norm_num
      have h1 :
          (46.97 : ℝ) * (46.97 : ℝ) < (46.97 : ℝ) * (phi ^ (8 : ℕ)) :=
        mul_lt_mul_of_pos_left h8_lo hpos4697
      have h2 :
          (46.97 : ℝ) * (phi ^ (8 : ℕ)) < (phi ^ (8 : ℕ)) * (phi ^ (8 : ℕ)) :=
        mul_lt_mul_of_pos_right h8_lo hpos8
      exact lt_trans h1 h2
    have h16_lo : (46.97 : ℝ) * (46.97 : ℝ) < phi ^ (16 : ℕ) := by
      simpa [hpow16] using h16_mul
    have h17_mul :
        ((46.97 : ℝ) * (46.97 : ℝ)) * (1.618 : ℝ) < (phi ^ (16 : ℕ)) * phi := by
      have hpos1618 : (0 : ℝ) < (1.618 : ℝ) := by norm_num
      have h1 :
          ((46.97 : ℝ) * (46.97 : ℝ)) * (1.618 : ℝ) < (phi ^ (16 : ℕ)) * (1.618 : ℝ) :=
        mul_lt_mul_of_pos_right h16_lo hpos1618
      have hpos16 : (0 : ℝ) < phi ^ (16 : ℕ) := by
        have hφ : 0 < phi := Constants.phi_pos
        exact pow_pos hφ _
      have h2 :
          (phi ^ (16 : ℕ)) * (1.618 : ℝ) < (phi ^ (16 : ℕ)) * phi :=
        mul_lt_mul_of_pos_left hφ_lo hpos16
      exact lt_trans h1 h2
    have h3500 : (3500 : ℝ) < ((46.97 : ℝ) * (46.97 : ℝ)) * (1.618 : ℝ) := by
      norm_num
    have h17_lo : ((46.97 : ℝ) * (46.97 : ℝ)) * (1.618 : ℝ) < phi ^ (17 : ℕ) := by
      simpa [hpow17] using h17_mul
    exact lt_trans h3500 h17_lo
  · -- Upper bound
    have h16_mul :
        (phi ^ (8 : ℕ)) * (phi ^ (8 : ℕ)) < (46.99 : ℝ) * (46.99 : ℝ) := by
      have hpos8 : 0 < phi ^ (8 : ℕ) := by
        have hφ : 0 < phi := Constants.phi_pos
        exact pow_pos hφ _
      have h1 :
          (phi ^ (8 : ℕ)) * (phi ^ (8 : ℕ)) < (46.99 : ℝ) * (phi ^ (8 : ℕ)) :=
        mul_lt_mul_of_pos_right h8_hi hpos8
      have hpos4699 : (0 : ℝ) < (46.99 : ℝ) := by norm_num
      have h2 : (46.99 : ℝ) * (phi ^ (8 : ℕ)) < (46.99 : ℝ) * (46.99 : ℝ) :=
        mul_lt_mul_of_pos_left h8_hi hpos4699
      exact lt_trans h1 h2
    have h16_hi : phi ^ (16 : ℕ) < (46.99 : ℝ) * (46.99 : ℝ) := by
      simpa [hpow16] using h16_mul
    have h17_mul :
        (phi ^ (16 : ℕ)) * phi < ((46.99 : ℝ) * (46.99 : ℝ)) * (1.6185 : ℝ) := by
      -- Step 1: multiply `phi^16 < 46.99^2` on the right by positive `phi`
      have hposφ : 0 < phi := Constants.phi_pos
      have h1 :
          (phi ^ (16 : ℕ)) * phi < ((46.99 : ℝ) * (46.99 : ℝ)) * phi :=
        mul_lt_mul_of_pos_right h16_hi hposφ
      -- Step 2: multiply `phi < 1.6185` on the left by positive `46.99^2`
      have hposB : 0 < ((46.99 : ℝ) * (46.99 : ℝ)) := by norm_num
      have h2 :
          ((46.99 : ℝ) * (46.99 : ℝ)) * phi <
            ((46.99 : ℝ) * (46.99 : ℝ)) * (1.6185 : ℝ) :=
        mul_lt_mul_of_pos_left hφ_hi hposB
      exact lt_trans h1 h2
    have h3600 : ((46.99 : ℝ) * (46.99 : ℝ)) * (1.6185 : ℝ) < (3600 : ℝ) := by
      norm_num
    have h17_hi : phi ^ (17 : ℕ) < ((46.99 : ℝ) * (46.99 : ℝ)) * (1.6185 : ℝ) := by
      simpa [hpow17] using h17_mul
    exact lt_trans h17_hi h3600
MEASURED ratio_mu_e_exp_value · IndisputableMonolith/Verification/MassComparison.lean
ratio_mu_e_exp_value · IndisputableMonolith/Verification/MassComparison.lean:319 
/-- The experimental ratio m_μ/m_e ≈ 206.768... -/
theorem ratio_mu_e_exp_value : (206 : ℝ) < ratio_mu_e_exp ∧ ratio_mu_e_exp < (207 : ℝ) := by
  unfold ratio_mu_e_exp m_mu_exp m_e_exp
  constructor <;> norm_num
MEASURED ratio_tau_e_exp_value · IndisputableMonolith/Verification/MassComparison.lean
ratio_tau_e_exp_value · IndisputableMonolith/Verification/MassComparison.lean:324 
/-- The experimental ratio m_τ/m_e ≈ 3477.2... -/
theorem ratio_tau_e_exp_value : (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

What this page does not claim

The mass predictions are not exact matches to experiment. The module does not prove that the phi-ladder is the true law of particle masses. The experimental values are not derived from Recognition Science.

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/Verification/MassComparison.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND