Masses Smverification All Fermion Masses Pos

The positivity theorem

In the Standard Model of particle physics, the twelve fundamental fermions (six quarks and six leptons) all have positive mass. The electron weighs about 0.511 MeV/c², the top quark about 173 GeV/c², and every other fermion sits somewhere between. Negative mass would break the theory's stability and its interpretation of vacuum energy, so positivity is a basic sanity condition on any mass formula.

The Recognition Science framework, a mathematical structure built from a discrete recognition ledger (a record of events with a forced cost function), predicts fermion masses through a specific formula: m(particle) = yardstick(Sector) × φ^(r - 8 + gap(Z)), where φ is the golden ratio, r is a rung index derived from cube geometry, and Z encodes charge structure. This formula has zero free parameters. The declaration all_fermion_masses_pos proves, in the framework's machine-checked library of formal theorems, that for every one of the nine charged fermions (electron, muon, tauon, up, charm, top, down, strange, bottom), the predicted mass is strictly greater than zero.

The proof is not a numerical check. It is a formal theorem: for all f : Fermion, 0 < fermionMass f. The library proves it by case analysis on each fermion, applying a general lemma predict_mass_pos that holds for every sector and rung. This means the positivity is a structural consequence of the mass law itself, not an accident of particular numbers. The theorem is one of three components in the framework's Standard Model verification certificate, alongside the φ-scaling law between generations and the count of nine charged fermions.

What the declaration does not claim is equally important. It does not assert that the predicted masses match the measured PDG 2024 values. That comparison is documented separately as hypotheses with experimental values, not as proved theorems. The lepton mass ratios agree with experiment to about 4-5%, but the quark ratios require additional gap corrections and are not formally verified. The declaration also does not claim that the mass formula itself is derived from first principles; the yardstick, rung, and gap parameters are derived from cube geometry and wallpaper groups, but their connection to physical measurement is an empirical check, not a theorem. Positivity is proved; numerical agreement is a stated hypothesis awaiting full interval arithmetic verification.

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

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

def sm_verification_cert : SMVerificationCert where
  all_positive := all_fermion_masses_pos
  phi_scaling := mass_rung_scaling
  nine_fermions := fermion_count

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 predicted masses match the measured PDG 2024 values; that comparison is stated as hypotheses, not proved theorems. The mass formula itself is derived from first principles; the yardstick, rung, and gap parameters are derived from geometry but their physical connection is empirical. The positivity theorem covers neutrinos; it applies only to the nine charged fermions in the Fermion inductive type.

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: