Foundation Qrft Fermion Kinetic Cert Fermion Kinetic Cert

The fermion kinetic certificate

The Standard Model describes fermions, the matter particles like electrons and quarks, with a Lagrangian: ψ̄(iγ^μ∂_μ − m)ψ. The first term is the kinetic energy of a free particle; the second, m ψ̄ψ, is the mass term. In Recognition Science, the framework maps this mass term to its cost, a forced penalty for recognition, and the kinetic term to a derivative on its discrete recognition lattice. The framework's library, a machine-checked collection of formal theorems, then certifies three structural facts about this mapping.

First, the number of fermions per generation is fixed: 15, matching the Standard Model's count of Weyl fermions. The certificate derives this as 5 electroweak sectors times 3 color copies, a structural forcing rather than an empirical input. Second, the mass at any rung k of the framework's ladder is m_k = m₀ · φ^k, where φ is the golden ratio. Third, adjacent rungs always share the same ratio: m_k+1 / m_k = φ. These three facts are packed into a single certificate object, built without any unproved assumptions or axioms.

The certificate does not claim to derive the Standard Model from scratch. It takes the framework's cost function and ladder as given, then shows that a specific mass spectrum follows. It does not predict the electron's mass; the base mass m₀ remains a free parameter. It does not prove that the Standard Model's measured masses actually sit on this ladder; that comparison against particle data is an empirical check, not a theorem. And the mapping of the Dirac operator to recognition-lattice derivatives is a definitional choice, not a derived result.

What the certificate does establish, within the framework, is internal consistency: the mass ladder's ratio is provably φ, the count is provably 15, and both follow from the same structural picture. This is a small but concrete step in the framework's larger program of deriving particle physics from recognition costs. The reader can now see exactly what is proved and what remains a modeling assumption.

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

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']

/-- Fermion kinetic sector certificate. -/
def fermionKineticCert : FermionKineticCert where
  fermions_per_gen := fermionsPerGeneration_val
  mass_pos := @fermionMassAt_pos
  mass_ratio := @fermionMassAt_adjacent_ratio

What this page does not claim

The certificate does not derive the Standard Model's measured masses from first principles. The Dirac operator mapping to recognition-lattice derivatives is a definitional choice, not a theorem. The certificate does not predict the electron mass or any specific fermion mass value.

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: