Standard Model Strong Cp

The strong CP problem

The strong nuclear force, which binds quarks into protons and neutrons, is described by a quantum field theory called quantum chromodynamics (QCD). The theory contains a parameter, usually written θ (theta), that measures how much the strong force violates a symmetry called CP, which roughly distinguishes matter from antimatter. A nonzero θ would mean the strong force treats particles and their mirror images differently, an effect that would show up as a tiny electric dipole moment in the neutron. Experiments place an extremely tight bound on this parameter: |θ| < 10⁻¹⁰. The puzzle is that nothing in QCD forces θ to be small; it could naturally be any value between 0 and 2π. The fact that it is so close to zero is called the strong CP problem.

Physicists have proposed several solutions. The most popular is the axion, a hypothetical particle whose field dynamically relaxes θ toward zero. Another idea posits a massless up quark, which would make θ unphysical, but measurements rule that out. A third approach invokes spontaneous CP violation, where θ starts at zero by construction. Each solution adds new physics beyond the Standard Model, and none has been confirmed experimentally.

In Recognition Science, the framework models the strong CP problem through its eight-tick structure. The framework's central idea is that recognition events, discrete records of interaction, come at a forced cost. From that cost function, a chain of theorems derives an eight-step cycle, and this cycle imposes discrete phase constraints on θ. The framework defines a cost function for θ as (1 − cos θ), which is minimized at θ = 0. The eight-tick structure quantizes the allowed values of θ to multiples of π/4: 0, π/4, π/2, and so on. Among these discrete choices, the cost function selects θ = 0 as the unique minimum, so the framework predicts θ = 0 exactly, well inside the experimental bound of 10⁻¹⁰.

This is a different kind of explanation from the axion. The axion is a continuous relaxation mechanism; the framework's account is a discrete selection rule. The framework does not require a new particle, though it is compatible with one. Its library of machine-checked theorems proves that θ = 0 minimizes the cost function and that this value lies within the experimental window. The framework's prediction is exact, not approximate, and it is falsifiable: a measured nonzero θ, a continuous axion solution, or a failure of the eight-tick structure would each refute the account.

theorem theta_zero_minimizes :
    ∀ θ, thetaJCost 0 ≤ thetaJCost θ := by
  intro θ
  unfold thetaJCost
  simp only [Real.cos_zero]
  linarith [Real.cos_le_one θ]

/-- In RS, θ is quantized by 8-tick symmetry:

    The allowed values are: θ = 2πk/8 = πk/4 for k ∈ {0,1,...,7}

    This gives only 8 allowed values:
    0, π/4, π/2, 3π/4, π, 5π/4, 3π/2, 7π/4 -/
noncomputable def allowedTheta : List ℝ := [0, π/4, π/2, 3*π/4, π, 5*π/4, 3*π/2, 7*π/4]

/-- |θ_RS| < 10⁻¹⁰ — RS satisfies the experimental bound trivially. -/
theorem abs_theta_RS_lt_bound :
    |theta_RS_predicted| < theta_experimental_max := by
  unfold theta_RS_predicted theta_experimental_max
  simp
  norm_num

What this page does not claim

The framework does not derive the axion or any new particle. The framework does not prove that the eight-tick structure is the only possible source of the bound. The framework does not claim to explain why θ is exactly zero in the absence of the cost-minimization argument.

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