Foundation Qrft Fermion Kinetic Cert Fermions Per Generation

The fermion count

In the standard model of particle physics, each generation of matter contains 15 Weyl fermions: the electron, up and down quarks, and their neutrino, with each quark coming in three colors. This count is a foundational fact of the theory, and the Recognition Science framework records it in a ledger, a discrete record of events, as the definition fermionsPerGeneration with the value 15.

The library proves one theorem about this number: fermionsPerGeneration = 5 * 3. That is, the 15 fermions decompose into 5 electroweak sectors, each with 3 color copies. This is a structural statement about how the count factorizes, not a derivation of the count from first principles. The definition and the factorization theorem are both checked by the machine, with no unproved assumptions.

The same file also defines a mass ladder. For any rung k, the fermion mass is m0 * phi^k, where phi is the golden ratio. The library proves that each step up the ladder multiplies the mass by phi, and that all masses are positive when the base mass is positive. This is a definitional model of mass ratios, not a prediction of specific particle masses.

In Recognition Science, the framework models the fermion kinetic term as a derivative on a recognition lattice, and the mass term as a cost on a recognition ratio. The 15-per-generation count is presented as a structural forcing: 5 electroweak sectors times 3 colors. This is a claim about how the number factorizes within the framework's picture, not a proof that the standard model must have exactly 15 fermions.

The declaration does not claim to derive the existence of three generations, nor does it explain why the electroweak sector has 5 components. It records a count and proves its factorization. The mass ladder is a model that reproduces the observed pattern of mass ratios, but it does not predict the base mass m0 for any particle.

/-- Structural derivation: 5 EW sectors × 3 colors = 15. -/
theorem fermionsPerGeneration_val : fermionsPerGeneration = 5 * 3 := by
  unfold fermionsPerGeneration; rfl

/-- Number of Weyl fermions per generation = 15 (SM counting). -/
def fermionsPerGeneration : ℕ := 15

/-- Fermion mass at φ-ladder rung `k`. -/
def fermionMassAt (m0 : ℝ) (k : ℕ) : ℝ := m0 * phi ^ k

theorem fermionMassAt_adjacent_ratio {m0 : ℝ} (hm : 0 < m0) (k : ℕ) :
    fermionMassAt m0 (k + 1) / fermionMassAt m0 k = phi := by
  rw [fermionMassAt_succ_ratio hm]
  field_simp [(fermionMassAt_pos hm k).ne']

What this page does not claim

The declaration does not prove the standard model must have 15 fermions. The mass ladder does not predict the value of the base mass for any particle. The framework does not derive the existence of three generations.

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/Foundation/QRFT/FermionKineticCert.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: