Foundation Ckmhierarchy From Phi Ladder Quark Rungs Strict Ordering

The quark mass ladder

The Standard Model's six quarks have masses that span about five orders of magnitude, from the up quark near 2.2 MeV to the top quark near 173 GeV. The pattern among these masses has no explanation within the Standard Model itself. The Recognition Science framework proposes one: place each quark on a rung of a ladder where each step multiplies mass by the golden ratio φ, about 1.618. The declaration quark_rungs_strict_ordering is the formal statement that the six rungs are strictly ordered, from the lightest up quark to the heaviest top quark.

The framework assigns specific integer rungs to the quarks: up at 8, down at 9, strange at 14, charm at 17, bottom at 22, and top at 30. The strict ordering theorem proves these rungs satisfy 8 < 9 < 14 < 17 < 22 < 30. Because the framework also proves that mass at a rung equals a base unit times φ raised to the rung number, and that this function strictly increases with the rung, the ordering of rungs forces the ordering of masses. The theorem is checked in a machine-checked library of formal theorems, with no unproved assumptions.

The framework's mass formula is m(k) = m_unit · φ^k. The top-to-up mass ratio is therefore φ^(30-8) = φ^22, approximately 39,089. The measured ratio is about 80,000, within a factor of two of this prediction. The framework ascribes the discrepancy to a scale-running correction. The strict ordering theorem itself does not depend on this numerical match; it is a purely formal statement about the assigned rungs.

In Recognition Science, the rung positions are not arbitrary. They are said to be forced by the gauge structure SU(3)×SU(2)×U(1) on a three-dimensional space. The framework models the six quark masses as sitting on this φ-ladder, and the strict ordering theorem is a consequence of that model. It is a structural claim about the framework's own construction, not an empirical measurement.

The theorem's value is that it makes the framework's mass hierarchy precise and checkable. A falsifier exists: a precision quark-mass measurement off its predicted rung by more than about 0.118 log-mass units, or detection of a fourth generation of quarks, would break the ladder. This is a concrete prediction, not a post-hoc fit.

/-- Strict mass ordering: u < d < s < c < b < t. -/
theorem quark_rungs_strict_ordering :
    up_rung < down_rung ∧
    down_rung < strange_rung ∧
    strange_rung < charm_rung ∧
    charm_rung < bottom_rung ∧
    bottom_rung < top_rung := by
  refine ⟨?_, ?_, ?_, ?_, ?_⟩
  · unfold up_rung down_rung; norm_num
  · unfold down_rung strange_rung; norm_num
  · unfold strange_rung charm_rung; norm_num
  · unfold charm_rung bottom_rung; norm_num
  · unfold bottom_rung top_rung; norm_num

/-- Up-quark rung (lightest, first-generation up-type). -/
def up_rung : ℕ := 8

/-- Mass strictly increasing in rung count. -/
theorem mass_strict_increasing
    {m_unit : ℝ} (h_pos : 0 < m_unit) {k m : ℕ} (h : k < m) :
    mass_at_rung m_unit k < mass_at_rung m_unit m := by
  unfold mass_at_rung
  have h_phi : 1 < phi := one_lt_phi
  have h_pow : phi ^ k < phi ^ m := pow_lt_pow_right₀ h_phi h
  exact mul_lt_mul_of_pos_left h_pow h_pos

/-- The top-to-up mass ratio: `φ^(top_rung - up_rung) = φ^22`. -/
def mass_ratio_top_up : ℝ := phi ^ 22

What this page does not claim

This theorem does not predict any measured quark mass; it only orders the rungs. The framework does not derive the fine-structure constant alpha. The empirical ratio matching within a factor of two is not a theorem, but a check.

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/CKMHierarchyFromPhiLadder.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: