Physics Quark Masses

The quarter-ladder hypothesis

Quarks are the elementary particles that make up protons and neutrons. They come in six types, or flavors: up, down, strange, charm, bottom, and top. Each flavor has a distinct mass, from the light up quark at about 2.2 MeV/c² to the heavy top quark at about 173 GeV/c², a span of nearly a hundred thousand times. These masses are not predicted by the Standard Model of particle physics; they are measured inputs. The question of why quarks have the masses they do is one of the open problems in fundamental physics.

The standard approach to quark masses involves the Higgs mechanism and quantum chromodynamics (QCD), the theory of the strong force. The measured values come from experiments at particle colliders, with the most recent cost compilation from the Particle Data Group (PDG) in 2022. The top quark mass, for instance, is measured at 172,690 MeV/c², while the up quark is far lighter at 2.16 MeV/c². Because quarks are never observed in isolation, their masses are extracted indirectly from the properties of hadrons, the composite particles they form.

Recognition Science offers a different starting point. Its framework derives a single structural mass shared by all fermions, and arranges particles on a ladder of discrete steps. The step size is the golden ratio φ ≈ 1.618. Leptons, the electron and its heavier cousins, sit on integer rungs of this ladder. The quark hypothesis proposes that quarks occupy quarter-integer rungs instead. The idea is that quarks use the same underlying mass scale but at fractional positions, producing their distinct, heavier masses.

In this account, the predicted mass of a quark is m = m_struct × φ^R, where m_struct is the shared structural base and R is the rung number. The module assigns specific quarter-integer rungs to each quark: top at R = 5.75, bottom at R = -2.00, charm at R = -4.50, strange at R = -10.00, down at R = -16.00, and up at R = -17.75. These positions are not arbitrary; they follow from the spacing between generations, which the module states as steps of 7.75, 2.50, and 5.50 rungs between successive flavors.

What the module actually proves is limited. A machine-checked theorem verifies that the rungs derived from these steps match the stated ideal positions. The match between predicted and measured masses, however, is not a theorem. It is an explicit hypothesis, tagged as such in the code. The module defines predicates for how close each prediction comes to the PDG value, and provides a certificate structure that assembles these matches. For the top, bottom, and charm quarks, the claimed agreement is within 0.05%, 1%, and 2% respectively. But these are stated as empirical claims, not proven results.

The light quarks, strange, down, and up, show larger discrepancies, around 5% for strange and down and 2% for up. The module attributes these gaps to non-perturbative QCD effects, specifically chiral symmetry breaking, which are not yet included in this bare geometric derivation. The heavy quarks, less affected by the strong force, fit better. The framework's library explicitly marks this file as a hypothesis lane, not part of its parameter-free core mass model, until a full reconciliation is proven. The quark masses remain a target, not an achievement.

/-- Predicted Mass Formula: m = m_struct * phi^res. -/
noncomputable def predicted_mass (res : ℚ) : ℝ :=
  electron_structural_mass * (phi ^ (res : ℝ))

/-- **THEOREM: Quark Residues Match Steps**
    Verifies that the residues derived from steps match the ideal positions. -/
theorem residues_match_steps :
    res_bottom = -2 ∧ res_charm = -4.5 ∧ res_strange = -10 := by
  constructor
  · unfold res_bottom res_top step_top_bottom; norm_num
  constructor
  · unfold res_charm res_bottom res_top step_top_bottom step_bottom_charm; norm_num
  · unfold res_strange res_charm res_bottom res_top step_top_bottom step_bottom_charm step_charm_strange; norm_num

/-- **CERTIFICATE (HYPOTHESIS LANE)**: Quark Quarter-Ladder matches (top/bottom/charm). -/
structure QuarkMassCert where
  top_match : H_top_mass_match
  bottom_match : H_bottom_mass_match
  charm_match : H_charm_mass_match

def H_top_mass_match : Prop :=
  abs (predicted_mass res_top - mass_top_exp) / mass_top_exp < 0.0005

What this page does not claim

The quark mass predictions are not proven theorems; they are empirical hypotheses with named tolerances. This module does not derive the fine-structure constant or any coupling constant. No claim is made that the light-quark discrepancies are fully explained by QCD effects.

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/Physics/QuarkMasses.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: