Foundation Qrft Fermion Kinetic Cert Fermions Per Generation Val

The count of fermions

In particle physics, each generation of matter contains fifteen Weyl fermions: the electron, its neutrino, and two heavier charged leptons, each coming in three colors, plus the quarks. The standard model counts them one by one. The Recognition Science framework's declaration fermionsPerGeneration_val states that this count is not an accident but a product: 5 times 3 equals 15.

The number 5 comes from the framework's recognition structure, a discrete record of events where each step costs a fixed amount. At the spatial dimension D equals 3, the framework's configuration space has five electroweak sectors. Each sector carries three color copies, giving the fifteen Weyl fermions. The declaration is a theorem in the machine-checked library of formal theorems, proved by unfolding a definition and simplifying: it states that the number 15 equals 5 times 3.

The same file defines the fermion mass at a ladder rung k as m0 times phi to the k, where phi is the golden ratio. Two further theorems prove that this mass is always positive for a positive starting mass, and that the ratio of masses at adjacent rungs is exactly phi. These are separate claims; the declaration about the count of fermions does not depend on them.

What the declaration does not claim is that the standard model's fifteen fermions are the only possible count, or that the framework derives the observed mass values themselves. It establishes an arithmetic identity: the count 15 factors as 5 times 3. The physical identification of the five electroweak sectors and the three colors is a modeling choice, not a theorem. The mass ladder gives the ratio between rungs, not the absolute scale m0.

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

/-- 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 that fifteen is the only possible count of fermions per generation. It does not derive the measured mass values, only the ratio between adjacent ladder rungs. The identification of the five electroweak sectors and three colors is a modeling choice, not a derived theorem.

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: