Masses Verification Tau Electron Ratio Error

The tau-electron ratio check

The tau lepton is a heavy cousin of the electron, about 3,477 times more massive. In the Recognition Science framework, particle masses are not free parameters: they sit on a ladder of powers of the golden ratio, and the framework's machine-checked library of formal theorems verifies the arithmetic that connects those powers to measured masses. The declaration tau_electron_ratio_error is part of that verification effort. It does not, by itself, prove that the framework's mass formula is correct. What it does is establish a precise, checked relationship between a predicted ratio and the experimental ratio.

The experimental ratio of the tau mass to the electron mass, using the PDG 2024 values of 1776.86 MeV and 0.51099895069 MeV respectively, is defined as ratio_tau_e_exp. The framework's prediction for the tau mass, tau_pred, is given by the formula φ⁷⁶ / 4194304000000 MeV, where φ is the golden ratio. The key theorem tau_ratio_overshoot proves that this experimental ratio is less than φ¹⁷. In plain terms, the framework's predicted ratio for the tau to the electron overshoots the measured value. The theorem pins down that overshoot to a specific bound: the measured ratio sits below the golden ratio to the seventeenth power, a number near 3571. This is a numerical fact, machine-checked, about where the prediction stands relative to experiment.

The declaration's power is in its precision and its limits. It does not claim the prediction is correct, nor does it assign a percentage error. It establishes a single, exact inequality. The measured ratio is known to lie between 3477 and 3478, while the golden ratio to the seventeenth power is between 3569 and 3574. The theorem tau_ratio_overshoot proves the former is less than the latter. This is a check, not an endorsement. The framework's own documentation quarantines this comparison from its certified surface, noting that experimental values are imported constants, not derived from the framework. The declaration therefore serves as an honest, machine-verified record of how a specific prediction fares against a specific measurement, without overstating what that comparison means.

noncomputable def ratio_tau_e_exp : ℝ := m_tau_exp / m_e_exp

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

private lemma phi17_gt : (3569 : ℝ) < Constants.phi ^ (17 : ℕ) := by
  rw [phi_eq_goldenRatio]
  have h8_lo := Numerics.phi_pow8_gt
  have hφ_lo := Numerics.phi_gt_1618
  have hpos8 : (0 : ℝ) < Real.goldenRatio ^ 8 := by positivity
  have hpos16 : (0 : ℝ) < Real.goldenRatio ^ 8 * Real.goldenRatio ^ 8 := by positivity
  have heq : Real.goldenRatio ^ 17 = Real.goldenRatio ^ 8 * Real.goldenRatio ^ 8 * Real.goldenRatio := by ring_nf
  rw [heq]
  have h16_lo : (46.97 : ℝ) * (46.97 : ℝ) < Real.goldenRatio ^ 8 * Real.goldenRatio ^ 8 :=
    mul_lt_mul h8_lo (le_of_lt h8_lo) (by norm_num) (le_of_lt hpos8)
  have h17_lo : (46.97 : ℝ) * (46.97 : ℝ) * (1.618 : ℝ) <
      Real.goldenRatio ^ 8 * Real.goldenRatio ^ 8 * Real.goldenRatio :=
    mul_lt_mul h16_lo (le_of_lt hφ_lo) (by norm_num) (le_of_lt hpos16)
  linarith [show (3569 : ℝ) < (46.97 : ℝ) * (46.97 : ℝ) * (1.618 : ℝ) from by norm_num]

private lemma phi17_lt : Constants.phi ^ (17 : ℕ) < (3574 : ℝ) := by
  rw [phi_eq_goldenRatio]
  have h8_hi := Numerics.phi_pow8_lt
  have hφ_hi := Numerics.phi_lt_16185
  have hpos8 : (0 : ℝ) < Real.goldenRatio ^ 8 := by positivity
  have hφ_pos : (0 : ℝ) < Real.goldenRatio := by simpa using Real.goldenRatio_pos
  have heq : Real.goldenRatio ^ 17 = Real.goldenRatio ^ 8 * Real.goldenRatio ^ 8 * Real.goldenRatio := by ring_nf
  rw [heq]
  have h16_hi : Real.goldenRatio ^ 8 * Real.goldenRatio ^ 8 < (46.99 : ℝ) * (46.99 : ℝ) :=
    mul_lt_mul h8_hi (le_of_lt h8_hi) hpos8 (by norm_num)
  have h17_hi : Real.goldenRatio ^ 8 * Real.goldenRatio ^ 8 * Real.goldenRatio <
      (46.99 : ℝ) * (46.99 : ℝ) * (1.6185 : ℝ) :=
    mul_lt_mul h16_hi (le_of_lt hφ_hi) hφ_pos (by norm_num)
  linarith [show (46.99 : ℝ) * (46.99 : ℝ) * (1.6185 : ℝ) < (3574 : ℝ) from by norm_num]

What this page does not claim

The declaration does not prove the framework's mass formula is correct. The declaration does not assign a percentage error to the tau mass prediction. The declaration does not derive the experimental mass values from the framework.

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: