Foundation Qrft Fermion Kinetic Cert Fermion Mass At

The mass ladder

The Standard Model of particle physics treats the masses of quarks and leptons as free inputs: you measure them, then plug them into the Lagrangian. Recognition Science (RS) proposes instead that these masses are not arbitrary, but are constrained to lie on a geometric ladder. The declaration fermionMassAt defines that ladder: for a starting mass m₀ at rung 0, the mass at rung k is m₀ times φ raised to the power k, where φ is the golden ratio, approximately 1.618. The mass at each successive rung is exactly φ times the mass at the previous rung. This is a definition, not a measurement: it chooses the form of the ladder, and the choice is encoded in the machine-checked library of formal theorems.

The ladder's structure is proved. The library shows that if the starting mass is positive, every rung's mass is positive; and that the ratio of adjacent rungs is exactly φ. These are formal theorems, checked by the framework's kernel. The definition itself is a model: it asserts that fermion masses follow this pattern, but it does not derive the pattern from deeper principles. The physical claim, that the Standard Model spectrum actually sits on this ladder, is a prediction to be tested against measured masses, not a theorem.

The declaration also counts fermions. The Standard Model has 15 Weyl fermions per generation (16 with right-handed neutrinos). RS models this as 5 electroweak sectors times 3 color copies. That arithmetic, 5 times 3 equals 15, is proved in the library. But the identification of the electroweak sectors is a modeling choice, not a derivation from the forcing chain.

What fermionMassAt does not claim is the hard part. It does not claim that the measured masses of actual particles match the ladder. It does not assign a value to m₀; that remains a free parameter. It does not prove that the Standard Model spectrum is reproduced. The ladder is a structural template, and the template's fit to reality is an open empirical question. The framework's own honesty rules require saying that plainly: the scaling law is proved, the comparison against measured PDG values is a check, not a theorem.

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 mass at φ-ladder rung `k`. -/
def fermionMassAt (m0 : ℝ) (k : ℕ) : ℝ := m0 * phi ^ k

theorem fermionMassAt_pos {m0 : ℝ} (hm : 0 < m0) (k : ℕ) :
    0 < fermionMassAt m0 k := by
  unfold fermionMassAt
  exact mul_pos hm (pow_pos Constants.phi_pos k)

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

What this page does not claim

The measured masses of actual particles match the ladder. The base mass m₀ is derived from the framework. The Standard Model mass spectrum is reproduced by the ladder. The electroweak sector count is derived from the forcing chain.

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: