The Strong CP Problem: A Formal Treatment of QCD CP Violation and Axion Solutions

We present a formal treatment of the Strong CP problem in QCD and its solutions. The physical θ-parameter, which would induce CP violation through a neutron electric dipole moment, is bounded by experiment to |θ| < 10⁻¹⁰. We prove 15 theorems characterizing this puzzle: (1) the θ-EDM bound connecting theory to experiment; (2) the structure of θ_eff = θ_QCD + arg(det M_q) and its fine-tuning; (3) chiral invariance of θ_eff under U(1) rotations; (4) the Vafa-Witten theorem showing E(θ) ≥ E(0); (5) topological susceptibility χ_top > 0 confirming θ = 0 is a minimum; (6) exclusion of the massless quark solution by lattice QCD; (7) the strong/weak CP disparity; and the Peccei-Quinn solution: (8) dynamic θ relaxation via the axion field; (9) axion mass from QCD topology; (10) axion-photon coupling; (11) the axion window; (12) the PQ quality problem from gravity; (13) the Nelson-Barr alternative; and (14) the dual solution—axion as both CP solver and dark matter candidate. All proofs are machine-verified in the Platonic kernel (15/15 verified, 0 axioms beyond variable declarations).

Keywords: Strong CP problem, θ-vacuum, axion, Peccei-Quinn mechanism, QCD, CP violation, dark matter

MSC 2020: 81V05, 81T13, 83C47