Standard Model Proton Mass

The proton mass

The proton is a composite particle, a bound state of three valence quarks: two up quarks and one down quark. Its measured mass is about 938.3 MeV/c². The puzzle of the proton is that the quarks themselves account for only about one percent of that total. The rest comes from the energy of the strong force, the QCD binding energy that holds the quarks together. This is a standard result of quantum chromodynamics, established over decades of experiment and lattice computation.

The standard model does not predict the proton mass from first principles; it inputs the quark masses and the strong coupling constant, and the binding energy emerges from nonperturbative QCD. Recognition Science (RS) proposes a different route. In RS, particle masses sit on a ladder of powers of the golden ratio φ, where φ = (1 + √5)/2 ≈ 1.618. The framework models the valence quark contribution as three masses, each equal to a mass scale times φ raised to the power of a rung index. The proton's valence contribution sits at rung 4.

In Recognition Science, the framework derives the binding energy from the same ladder, not from a fitted parameter. The confinement rung is much higher, r_binding = 14. The separation in rungs is 10, so the binding energy is larger than the valence contribution by a factor of φ^10 ≈ 123. The framework proves, in its machine-checked library of formal theorems, that the binding energy is positive, that the total proton mass is positive, and that binding dominates the valence contribution by more than a factor of 40. The total proton mass is defined as the sum of the valence and binding contributions.

What this establishes in plain language is a structural claim: the proton's mass is not a free parameter in RS, but a sum of two terms, each tied to the same φ-ladder. The framework does not fit the binding energy; it derives it from the confinement rung. The numerical comparison to the measured 938.3 MeV is an empirical check, not a theorem. The framework's library proves the positivity and dominance relations, not the numerical value itself.

theorem E_binding_pos : 0 < E_binding := by
  unfold E_binding r_binding; exact mass_on_rung_pos 14

theorem m_p_pos : 0 < m_p := by
  unfold m_p; linarith [m_valence_pos, E_binding_pos]

theorem binding_dominates : E_binding > 40 * m_valence := by
  unfold E_binding m_valence m_u_contrib m_d_contrib r_binding mass_on_rung
  have hA : 0 < Masses.Anchor.E_coh := anchor_E_coh_pos
  have h14_eq : phi ^ (14 : ℤ) = phi ^ (4 : ℤ) * phi ^ (10 : ℤ) := by
    rw [← zpow_add₀ phi_ne_zero]; norm_num
  rw [h14_eq]
  have h4_pos : 0 < phi ^ (4 : ℤ) := zpow_pos phi_pos _
  have h10_gt : phi ^ (10 : ℤ) > (120 : ℝ) := by
    have h5_eq : phi ^ (10 : ℤ) = phi ^ (5 : ℤ) * phi ^ (5 : ℤ) := by
      rw [← zpow_add₀ phi_ne_zero]; norm_num
    rw [h5_eq]
    have h5_gt : phi ^ (5 : ℤ) > (11 : ℝ) := by
      rw [zpow_ofNat]
      have : phi ^ 5 = 5 * phi + 3 := by
        have h3 : phi ^ 3 = 2 * phi + 1 := by
          calc phi ^ 3 = phi * phi ^ 2 := by ring
            _ = phi * (phi + 1) := by rw [phi_sq_eq]
            _ = phi ^ 2 + phi := by ring
            _ = (phi + 1) + phi := by rw [phi_sq_eq]
            _ = 2 * phi + 1 := by ring
        calc phi ^ 5 = phi ^ 2 * phi ^ 3 := by ring
          _ = (phi + 1) * (2 * phi + 1) := by rw [phi_sq_eq, h3]
          _ = 2 * phi ^ 2 + 3 * phi + 1 := by ring
          _ = 2 * (phi + 1) + 3 * phi + 1 := by rw [phi_sq_eq]
          _ = 5 * phi + 3 := by ring
      rw [this]; linarith [phi_gt_onePointSixOne]
    nlinarith [h5_gt]
  have h_base := mul_pos hA h4_pos
  nlinarith [mul_lt_mul_of_pos_left h10_gt h_base]

What this page does not claim

The numerical value 938.3 MeV is not proved by the framework; it is an empirical comparison. The framework does not derive the quark masses themselves from the ladder; it places them at a rung. This module does not establish that the φ-ladder is the unique source of hadron masses.

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/StandardModel/ProtonMass.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: