Foundation Qrft Fermion Kinetic Cert Fermion Mass At Adjacent Ratio

The mass ladder

The golden ratio φ, roughly 1.618, is the number that solves r² = r + 1. In the Recognition Science framework, it appears as the unique self-similar scaling forced by the framework's core cost function. The declaration fermionMassAt_adjacent_ratio states a consequence of that forcing for the fermion mass ladder: for any positive base mass m₀ and any rung index k, the mass at rung k+1 divided by the mass at rung k equals φ exactly.

The mass at a rung is defined as m₀ · φᵏ. The theorem then says that moving up one rung multiplies the mass by φ, and moving down divides it by φ. This is a pure algebraic identity, proved in the machine-checked library of formal theorems. It holds for every integer rung k and every positive base mass m₀. The positivity condition matters: the ratio is only defined when the masses are nonzero, and the framework proves that a positive base mass yields positive masses at every rung.

The declaration is part of a larger structural claim. The framework models the Standard Model fermion kinetic Lagrangian, mapping the mass term to a cost on a recognition ratio and the kinetic term to a lattice derivative. It also derives the count of 15 Weyl fermions per generation as 5 electroweak sectors times 3 colors. The mass ladder is the same φ-ladder already proved in the mass-ratio modules, now applied to the fermion kinetic sector.

What the declaration does not claim is important. It does not state that any particular fermion mass equals a specific measured value. It does not fix the base mass m₀; that parameter is left free. The theorem is about the ratio between adjacent rungs, not about absolute masses. It also does not claim that the Standard Model itself is derived; it establishes a structural property of the framework's model of the fermion kinetic sector.

The practical consequence is a sharp prediction: if the framework's ladder is correct, then fermion masses across generations should cluster near φ-multiples of a common base. The ratio between a fermion mass and its next-generation partner should be close to φ. This is a testable pattern, though the base mass itself must be set by other means.

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

/-- 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 declaration does not identify any specific fermion's measured mass. The declaration does not derive the Standard Model itself. The declaration does not fix the value of the base mass m₀.

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: