Physics Hadrons

Hadron masses from rungs

Hadrons are composite particles, such as protons and pions, that are built from quarks held together by the strong force. In the standard picture, a meson is a quark-antiquark pair and a baryon is a three-quark state. Their masses are not predicted from first principles; they are inputs to the theory, measured experimentally and tabulated by the Particle Data Group.

In Recognition Science, the framework models a hadron as a pair of fermions (the quark-like constituents) together with an integer binding term. Each fermion carries a rung, a discrete level in the recognition ladder. The composite rung of a hadron is the sum of its two constituent rungs plus the binding integer. The hadron mass is then defined as a constant times the golden ratio raised to that composite rung. This is a definitional choice, not a derivation: the framework chooses this form, and the module does not yet prove that it reproduces the measured spectrum.

What the module does prove are structural facts. If two hadrons have the same composite rung, the theorem hadron_equal_z_degenerate forces their masses to be equal. This gives a formal statement of degeneracy, such as the near-equal masses of the rho and omega mesons. For Regge trajectories, the mass-squared formula m² = n α′ φ^(2r) is shown to be non-negative and linear in the excitation number n. These are the kernel-checked results: they hold by construction of the definitions, not by comparison with data.

The Regge slope α′ is not derived. The module carries a certificate structure with a placeholder value of 0.9 GeV⁻², labeled as a PDG-facing convention. This is an external seam, explicitly kept separate from the structural theorems. The docstring marks the entire module as Phase 6 scaffolding, out of scope for Level A completion. So the honest summary is: the framework defines a mass formula from rungs, proves internal consistency properties, and leaves the empirical validation as future work.

What this changes is the status of hadron masses in the framework. Instead of being free parameters, they become functions of a discrete counting structure. The framework does not yet claim to predict the proton mass or the rho-omega splitting; it claims a formal skeleton on which such predictions could hang. A reader should see this as a definitional scaffold with a few proved structural lemmas, not as a completed theory of hadron physics.

/-- Equal-Z hadrons are degenerate at leading order. -/
theorem hadron_equal_z_degenerate (h1 h2 : Hadron)
  (h_same_rung : composite_rung h1 = composite_rung h2) :
  hadron_mass h1 = hadron_mass h2 := by
  simp [hadron_mass, h_same_rung]

/-- Regge mass squared is non-negative. -/
theorem regge_mass_squared_nonneg (r n : ℕ) : regge_mass_squared r n pdg_regge_slope ≥ 0 := by
  have hphi_pow_nonneg : 0 ≤ Constants.phi ^ (2 * (r : ℝ)) :=
    le_of_lt (Real.rpow_pos_of_pos Constants.phi_pos _)
  have hslope_nonneg : (0 : ℝ) ≤ pdg_regge_slope := by
    norm_num [pdg_regge_slope, pdg_regge_slope_cert]
  have hn_nonneg : 0 ≤ (n : ℝ) := by exact_mod_cast (Nat.zero_le n)
  have h1 : 0 ≤ (n : ℝ) * pdg_regge_slope := mul_nonneg hn_nonneg hslope_nonneg
  have h2 : 0 ≤ (n : ℝ) * pdg_regge_slope * (Constants.phi ^ (2 * (r : ℝ))) :=
    mul_nonneg h1 hphi_pow_nonneg
  simpa [regge_mass_squared, pdg_regge_slope, mul_comm, mul_left_comm, mul_assoc] using h2

/-- Regge trajectory is linear in n. -/
theorem regge_linearity (r : ℕ) (n₁ n₂ : ℕ) :
    regge_mass_squared r (n₁ + n₂) pdg_regge_slope =
    regge_mass_squared r n₁ pdg_regge_slope + regge_mass_squared r n₂ pdg_regge_slope := by
  simp [regge_mass_squared]
  ring

noncomputable def hadron_mass (h : Hadron) : ℝ :=
  Constants.E_coh * (Constants.phi ^ (composite_rung h : ℝ))

-- Regge trajectory: excited states n=0,1,2,... m_n^2 = n α' φ^{2 r} (r=base rung)

What this page does not claim

The module does not prove that any measured hadron mass equals the rung-based formula. The Regge slope α′ is not derived; it is a placeholder certificate value. This is not a complete theory of hadron physics; the docstring marks it as Phase 6 scaffolding.

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