Masses Verification Mass Verification Cert Exists

A machine-checked comparison

The declaration mass_verification_cert_exists is a certificate inside a machine-checked library of formal theorems. It establishes that the library's own formulas for certain particle masses, based on powers of the golden ratio, fall within a stated percentage of the experimental values published by the Particle Data Group in 2024. The certificate is a formal object: a computer program has verified the arithmetic and the inequalities, so the comparison is not a hand-waved estimate but a checked proof.

The classical entry point is the lepton sector. The library defines a prediction for the electron, muon, and tau masses using a formula that combines powers of the golden ratio with powers of two and a million. For the muon, the certificate proves that the predicted mass differs from the measured value by less than four percent. For the proton, a separate prediction for its binding energy lands within 3.5 percent of the measured proton mass. These are the concrete claims: the numbers are close, and the closeness is machine-verified.

In Recognition Science, the framework models particle masses as sitting on a ladder where each rung is a power of the golden ratio. The scaling law is proved within the framework; the comparison against measured values is an empirical check, not a theorem. The certificate makes that check explicit and auditable. It does not turn the measurements into derived results. The experimental masses are imported constants, and the library's own documentation marks them as quarantined from the certified surface: they are inputs, not outputs.

What the certificate does not claim is as important as what it proves. It does not claim that the framework derives the measured masses from first principles. It does not claim that the four percent and 3.5 percent windows are tight enough to discriminate between the framework and other models. And it does not claim that the golden-ratio ladder is the only way to produce numbers near the measured values. The certificate is a bounded statement: given these imported measurements, these predictions, and these error thresholds, the inequalities hold.

The practical consequence is a template for honest comparison. A reader can see exactly what was checked, what was assumed, and where the boundary lies between derived structure and imported data. That boundary is the part that earns trust.

theorem muon_relative_error :
    |rs_mass_MeV .Lepton 13 - m_mu_exp| / m_mu_exp < 0.04 := by
  rw [muon_pred_eq]
  have hb := muon_mass_bounds
  have hexp_pos : (0 : ℝ) < m_mu_exp := by unfold m_mu_exp; norm_num
  rw [div_lt_iff₀ hexp_pos, abs_lt]
  unfold m_mu_exp
  constructor <;> nlinarith [hb.1, hb.2]

/-- The proton prediction (binding-dominated) is within 3.5% of the PDG value.

Note: the integer rung 48 is the closest to the proton mass. The ~3.3%
overshoot reflects the non-perturbative QCD binding that sits between
rungs 47 and 48 on the phi-ladder.

The proton mass is measured to 2.9e-7 MeV, so a 3.5% tolerance is about a hundred
million times the experimental resolution and this theorem is not a test. The
prediction is excluded by the measurement; see
`Masses.RungLadderExclusion.proton_pred_outside_window`. -/
theorem proton_relative_error :
    |proton_binding_pred - m_p_exp| / m_p_exp < 0.035 := by
  have hb := proton_mass_bounds
  have hexp_pos : (0 : ℝ) < m_p_exp := by unfold m_p_exp; norm_num
  rw [div_lt_iff₀ hexp_pos, abs_lt]
  unfold m_p_exp
  constructor <;> nlinarith [hb.1, hb.2]

def m_e_exp : ℝ := 0.51099895069

What this page does not claim

The framework does not derive the measured particle masses from first principles. The certificate does not claim the four percent window is a tight constraint on the framework. The golden-ratio ladder is not claimed to be the unique way to approximate the measured masses.

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: