strongCPCert
plain-language theorem explainer
The declaration constructs a certificate asserting that the J-cost of the QCD theta term reaches its global minimum exactly at θ=0, with all other allowed phases (multiples of π/4) carrying strictly positive cost. QCD phenomenologists and Recognition Science researchers would cite it to derive the observed |θ|<10^{-10} bound from eight-tick quantization without axions or fine-tuning. The construction is a direct record that applies the zero-minimizer lemma together with cosine evaluations at zero.
Claim. There exists a certificate such that the J-cost satisfies $1 - cos θ ≥ 0 = 1 - cos 0$ for every allowed phase θ, with equality if and only if θ = 0.
background
The module derives the strong CP problem from the eight-tick symmetry of Recognition Science. The QCD Lagrangian contains the term θ(g²/32π²)GμνG̃μν with θ ∈ [0,2π); eight-tick quantization restricts θ to multiples of π/4. The J-cost function is defined via the cost of recognition events (ObserverForcing.cost) and the derived cost of multiplicative recognizers (MultiplicativeRecognizerL4.cost), yielding thetaJCost(θ) = 1 − cos θ. Upstream results establish that recognition costs are nonnegative and that the fundamental time quantum is one tick.
proof idea
The definition builds the StrongCPCert structure by setting the minimizer field to the sibling lemma theta_zero_minimizes. Zero cost is verified by unfolding thetaJCost and simplifying with cos(0) = 1. The nonzero-positive field proceeds by assuming a positive cost and nonzero θ, unfolding thetaJCost, and using simp to obtain a contradiction from the cosine identity.
why it matters
This supplies the exact structural certificate θ_QCD = 0 required by the module's RS mechanism for the strong CP problem. It directly feeds the numerical bound bridge that combines the zero minimum with eight-tick quantization to obtain J-cost ≥ 1 − cos(π/4) > 0.29 for nonzero allowed values. The result aligns with the eight-tick octave (T7) and J-uniqueness (T5) while closing the structural half of the strong-CP explanation; the companion numerical interval theorem then bridges to the experimental neutron-EDM bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.