Masses Smverification Charged Fermion Generations

The generation count

The Standard Model of particle physics describes matter as made of fermions, particles with half-integer spin. These come in two families: quarks, which feel the strong force, and leptons, which do not. Both families are organized into three generations, each a heavier copy of the previous one. The electron, muon, and tauon are the three charged leptons; the up, charm, and top are the three up-type quarks; the down, strange, and bottom are the three down-type quarks. That makes nine charged fermions in total, or three generations times three particles per generation.

In the Recognition Science framework, this structure is captured by a machine-checked library of formal theorems. One declaration, charged_fermion_generations, states the arithmetic fact that 3 × 3 = 9. It is a theorem in the library's formal system, proved by computation. The declaration does not derive the existence of three generations from deeper principles; it simply records that the framework's enumeration of charged fermions, which it calls the Fermion type, has exactly nine members. The framework's ledger, a discrete record of particle species, lists these nine and no others.

The framework goes further and proves that all nine predicted masses are positive numbers, and that moving from one generation to the next multiplies a mass by the golden ratio φ ≈ 1.618. These are separate theorems in the library. The generation-count declaration itself, however, is only about the number nine. It does not claim that the framework explains why there are three generations, nor does it compare the predicted masses to experimental values. Those comparisons, when they exist, are stated separately as hypotheses with documented experimental data, not as theorems.

What the declaration does establish is a clean internal consistency check. The framework's model of particle species, built from its geometric and charge structure, yields exactly the nine charged fermions that the Standard Model's three-generation pattern requires. The arithmetic is trivial, but the fact that the framework's enumeration lands on nine, rather than eight or ten, is a meaningful alignment between the framework's internal logic and the observed particle content of the universe.

theorem charged_fermion_generations : 3 * 3 = (9 : ℕ) := by norm_num

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

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

theorem muon_rung_minus_electron_rung :
    r_lepton "mu" - r_lepton "e" = 11 := by
  simp only [r_lepton, tau, Anchor.E_passive, passive_field_edges,
             cube_edges, active_edges_per_tick, D, wallpaper_groups]
  norm_num

What this page does not claim

The declaration does not derive the existence of three generations from deeper principles. The declaration does not compare predicted masses to experimental values. The declaration does not claim that the framework explains the pattern of fermion 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/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: