StrongCPCert
plain-language theorem explainer
StrongCPCert packages the three properties that establish the J-cost reaches its global minimum of zero exclusively at θ = 0. Physicists modeling the strong CP problem inside Recognition Science cite this to derive the observed θ_QCD ≈ 0 from eight-tick phase constraints. The properties follow directly from the explicit definition thetaJCost(θ) = 1 − cos θ.
Claim. Let $J(θ) = 1 - cos θ$. Then $J(θ) ≥ J(0) = 0$ for all real θ, with equality if and only if θ = 0.
background
The module treats the strong CP problem as a consequence of eight-tick symmetry. The QCD angle θ must be a multiple of π/4; the J-cost then selects θ = 0. J-cost is defined in the sibling declaration thetaJCost as the real-valued function 1 − cos θ, which is nonnegative and vanishes only at multiples of 2π. The upstream result thetaJCost records that θ = 0 and θ = π are the CP-conserving points of lowest cost.
proof idea
The structure is a definition that bundles three statements already proved for the cosine expression. theta_minimizes and zero_cost are immediate from the range of cosine; nonzero_positive follows by contraposition once the minimum value is known to be zero.
why it matters
This certificate supplies the mathematical content for the claim that eight-tick symmetry forces θ_QCD = 0, closing the fine-tuning gap noted in the module. It is instantiated by the downstream definition strongCPCert, which assembles the three fields from prior lemmas theta_zero_minimizes and the cosine evaluation at zero. The construction sits inside the T7 eight-tick octave step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.