Foundation Ckmhierarchy From Phi Ladder Ckm Hierarchy One Statement

The quark mass ladder

The six quarks, the building blocks of protons and neutrons, have masses that range from about 2 MeV for the up quark to about 173 GeV for the top quark, a span of roughly five orders of magnitude. The Standard Model of particle physics measures these masses and the related mixing angles, but it does not explain why they take these particular values. The declaration ckm_hierarchy_one_statement is a machine-checked theorem in the Recognition Science framework that offers a structural answer: it places the quark masses on a geometric ladder, where each step multiplies the previous mass by a fixed ratio.

The ratio is the golden ratio φ, approximately 1.618, a number known since antiquity for its appearance in geometry and art. The theorem states that the mass of a quark at rung k is m_unit · φ^k, where m_unit is a framework-internal unit mass. The six known quarks are assigned to integer rungs: up at rung 8, down at 9, strange at 14, charm at 17, bottom at 22, and top at 30. The theorem proves three things about this arrangement: there are exactly six quarks, their rungs are strictly ordered by mass, and the ratio between adjacent rungs is exactly φ. It also proves that the top-to-up mass ratio, φ^22, is greater than 30,000.

The framework's claim is structural, not a precise numerical prediction. The empirical ratio of top to up quark masses is about 80,000, while φ^22 is about 39,089. The framework ascribes this factor-of-two discrepancy to a scale-running correction, but that correction is not part of the theorem. The theorem itself establishes the geometric structure: a fixed ratio between adjacent mass rungs, a strict ordering, and a lower bound on the extreme ratio. It does not derive the specific rung assignments from first principles; those are definitional choices within the framework, not consequences of the theorem.

In plain terms, the declaration proves that if quark masses follow the framework's recognition geometry, they must lie on a φ-ladder with six rungs, strictly ordered, with each step a factor of φ. This is a precise structural statement, machine-checked for internal consistency. What it does not do is prove that the empirical quark masses match this ladder exactly, nor does it explain why the rung numbers are 8, 9, 14, 17, 22, and 30. Those assignments are part of the framework's model, not forced by the theorem.

/-- Mass at rung `k`, parameterised by base mass unit. -/
def mass_at_rung (m_unit : ℝ) (k : ℕ) : ℝ := m_unit * phi ^ k

/-- **CKM HIERARCHY FROM φ-LADDER: ONE-STATEMENT THEOREM
(Track F7).**

The Standard Model six-quark mass hierarchy sits on the φ-rung
ladder with rungs (u: 8, d: 9, s: 14, c: 17, b: 22, t: 30). The
top-to-up ratio is `φ^22 > 39,000`, within a factor 2 of the
empirical 80,000. Strict mass ordering forced by ladder
monotonicity; per-rung ratio is exactly `φ`. -/
theorem ckm_hierarchy_one_statement :
    -- (1) Six quarks.
    quark_count = 6 ∧
    -- (2) Strict mass ordering.
    (up_rung < down_rung ∧
      down_rung < strange_rung ∧
      strange_rung < charm_rung ∧
      charm_rung < bottom_rung ∧
      bottom_rung < top_rung) ∧
    -- (3) Per-rung ratio is φ.
    (∀ m_unit k, mass_at_rung m_unit (k + 1) =
      mass_at_rung m_unit k * phi) ∧
    -- (4) Top-to-up ratio above 30,000.
    30000 < mass_ratio_top_up :=
  ⟨rfl,
   quark_rungs_strict_ordering,
   mass_geometric,
   mass_ratio_top_up_above_30000⟩

/-- Numerical lower bound: `φ^22 > 30,000` (within a factor 3 of
empirical 80,000 top-to-up mass ratio). We use that `1.61^22 > 30000`
via piecewise computation. -/
theorem mass_ratio_top_up_above_30000 : 30000 < mass_ratio_top_up := by
  unfold mass_ratio_top_up
  have h_phi : 1.61 < phi := phi_gt_onePointSixOne
  have h_pos : (0 : ℝ) ≤ 1.61 := by norm_num
  have h_pow : (1.61 : ℝ) ^ 22 ≤ phi ^ 22 :=
    pow_le_pow_left₀ h_pos (le_of_lt h_phi) 22
  -- (1.61)^22 = (1.61)^11 · (1.61)^11; (1.61)^11 ≈ 187.4
  -- (1.61)^11 > 175
  have h_11 : (175 : ℝ) < (1.61 : ℝ) ^ 11 := by
    have : (1.61 : ℝ) ^ 11 = 1.61 * 1.61 * 1.61 * 1.61 * 1.61 * 1.61 *
                              1.61 * 1.61 * 1.61 * 1.61 * 1.61 := by
      ring
    rw [this]; norm_num
  -- (1.61)^22 = ((1.61)^11)^2 > 175^2 = 30625
  have h_22 : (1.61 : ℝ) ^ 22 = ((1.61 : ℝ) ^ 11) ^ 2 := by ring
  have h_compute : (30000 : ℝ) < ((1.61 : ℝ) ^ 11) ^ 2 := by
    have h_11_pos : (0 : ℝ) < (1.61 : ℝ) ^ 11 := by positivity
    have h_sq_lt : (175 : ℝ)^2 ≤ ((1.61 : ℝ) ^ 11) ^ 2 := by
      have h_175_pos : (0 : ℝ) ≤ 175 := by norm_num
      exact pow_le_pow_left₀ h_175_pos (le_of_lt h_11) 2
    have h_175_sq : (175 : ℝ) ^ 2 = 30625 := by norm_num
    linarith
  rw [← h_22] at h_compute
  linarith

What this page does not claim

The theorem does not prove that the empirical quark masses exactly match the φ-ladder values; the top-to-up ratio is within a factor of two, not exact. The theorem does not derive the specific rung assignments (8, 9, 14, 17, 22, 30) from the recognition geometry; they are definitional choices. The theorem does not predict the absolute values of quark masses, only their ratios along the ladder.

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: