Masses Smverification

The mass verification module

The Standard Model of particle physics lists nine charged fermions: the electron, muon, and tauon leptons, plus six quarks. Each has a measured mass, from the electron at 0.511 MeV to the top quark near 172,760 MeV. Recognition Science (RS) asks whether these numbers fall into a pattern forced by its own structure. The mass verification module, a machine-checked collection of formal theorems, states the RS prediction for every fermion and documents how it lines up with the Particle Data Group's 2024 values.

The prediction uses one formula for all nine particles. A particle's mass equals a sector constant times the golden ratio φ raised to a power determined by its rung and charge gap. The sector constant comes from cube geometry and wallpaper groups, the rung from a counting of edges, and the charge gap from electric charge. Nothing is fitted. The module proves that every predicted mass is positive and that stepping up one rung multiplies the mass by φ, the same ratio that appears throughout RS structure.

The comparison with experiment works best for ratios between generations. The muon-to-electron mass ratio is predicted near φ¹¹ ≈ 199.0, against a measured 206.8, a difference of about 4 percent. The tauon-to-electron ratio lands near φ¹⁷ ≈ 3571, against 3477, roughly 3 percent off. Quark ratios need additional gap corrections and match less closely. The module states these comparisons as hypotheses with documented experimental values, not as proven equalities.

The module also counts the fermions it describes. A theorem proves there are exactly nine charged fermions in the framework's list, matching the three generations of three charged species. The certificate bundles the positivity proof, the φ-scaling law, and the count into one structure. What the module does not do is claim the numerical agreement is exact. Full numerical verification against experiment would require interval arithmetic on φ powers, which remains unfinished.

In plain terms, the module shows that a single φ-based ladder, with no adjustable parameters, reproduces the lepton mass ratios to a few percent and organizes all nine charged fermions into a coherent pattern. The gap between prediction and measurement is real and documented. The framework's claim is that the ladder is forced by its own geometry, not that the ladder already matches every digit of the Particle Data Group tables.

theorem all_fermion_masses_pos : ∀ f : Fermion, 0 < fermionMass f := by
  intro f; cases f <;> exact predict_mass_pos _ _ _

def fermionRung : Fermion → ℤ
  | .electron => r_lepton "e"
  | .muon => r_lepton "mu"
  | .tauon => r_lepton "tau"
  | .up => r_up "u"
  | .charm => r_up "c"
  | .top => r_up "t"
  | .down => r_down "d"
  | .strange => r_down "s"
  | .bottom => r_down "b"

theorem fermion_count : Fintype.card Fermion = 9 := by native_decide

theorem pdg_mu_e_ratio_approx : abs (pdg_mu_e_ratio - 206.8) < 1 := by
  simp only [pdg_mu_e_ratio, pdg_muon_MeV, pdg_electron_MeV]
  norm_num

What this page does not claim

The numerical agreement with PDG values is not proven exact, only stated as hypotheses. The module does not derive the sector constants from first principles within this file. No claim is made that the framework's mass formula has been checked against all measured digits.

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/SMVerification.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: