theta_zero_minimizes
plain-language theorem explainer
The declaration establishes that the J-cost for the QCD vacuum angle reaches its global minimum at θ = 0. Particle physicists studying the strong CP problem would cite it to ground the observed |θ| < 10^{-10} in Recognition Science's discrete phase constraints. The proof is a short term-mode argument that unfolds the cost definition and closes via the elementary bound cos θ ≤ 1 together with linear arithmetic.
Claim. $J_θ(0) ≤ J_θ(θ)$ for every real θ, where $J_θ$ denotes the J-cost of the QCD vacuum angle induced by the 8-tick phase structure.
background
The StandardModel.StrongCP module derives the smallness of θ_QCD from 8-tick symmetry. The QCD Lagrangian contains the CP-violating term θ (g²/32π²) G_μν G̃^μν with θ ∈ [0, 2π), yet experiment forces |θ| < 10^{-10}. Recognition Science restricts phases to multiples of π/4 via the eight-tick structure and selects θ = 0 by J-cost minimization.
proof idea
The proof is a one-line term-mode wrapper. It introduces arbitrary θ, unfolds thetaJCost, simplifies with cos(0) = 1, and applies linarith to the standard inequality cos θ ≤ 1.
why it matters
The result supplies the minimization property required by strongCPCert and strongCPNumericalCert. It realizes the RS mechanism in the module documentation: J-cost minimization under 8-tick symmetry selects phase zero. The argument connects directly to the eight-tick octave (T7) in the forcing chain and to the cost definitions in ObserverForcing and MultiplicativeRecognizerL4.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.