theta_qcd_cost_minimized_at_zero
plain-language theorem explainer
For every real angle θ, the quantity 1 − cos θ is nonnegative, so the effective J-cost of the QCD vacuum is minimized uniquely at θ_QCD = 0. Anyone citing the RS resolution of the Strong CP problem (energetic forcing of θ_QCD versus topological protection of δ_CKM) needs this inequality. The proof is a one-step appeal to cos θ ≤ 1 followed by linear arithmetic.
Claim. For every real number $\theta$, one has $0 \le 1 - \cos\theta$. In the RS effective cost $J_{\mathrm{eff}}(\theta) = J_0 + \Delta(1 - \cos\theta)$ with $\Delta > 0$, this forces the unique minimum at $\theta_{\mathrm{QCD}} = 0$.
background
The module derives the CKM CP phase from Berry phases accumulated by generation eigenstates on the directed 8-tick Gray-code cycle of the cube $Q_3$. The central distinction is energetic versus topological: $\theta_{\mathrm{QCD}}$ is an energetic vacuum angle, while $\delta_{\mathrm{CKM}}$ is a geometric Berry combination that chirality and directed traversal keep nonzero.
In Recognition Science the QCD vacuum angle enters an effective cost of the form $J_{\mathrm{eff}}(\theta) = J_0 + \Delta(1 - \cos\theta)$, where $\Delta > 0$ is the instanton-induced gap. The underlying cost is the standard RS $J$-cost (the unique solution of the Recognition Composition Law forced at T5), specialized here to a pure phase deviation from the vacuum. Nonnegativity of $1 - \cos\theta$ is exactly the statement that any nonzero $\theta$ raises the cost above $J_0$.
Upstream cost infrastructure (observer $J$-cost on recognition events, multiplicative-recognizer derived cost, PRC quotient cost) supplies the ambient meaning of "cost," but the present claim uses only the elementary bound on cosine.
proof idea
Introduce an arbitrary real $\theta$. Invoke the standard Mathlib fact $\cos\theta \le 1$. Rearrange by linear arithmetic to obtain $0 \le 1 - \cos\theta$. No RS-specific lemmas are required; the argument is pure real analysis.
why it matters
This is the energetic half of the RS Strong CP resolution. It is packaged with the topological half (cp_phase_nonzero) into strong_cp_resolved_with_ckm_cp, which asserts both $\forall\theta,,0\le 1-\cos\theta$ and $\delta_{\mathrm{CKM}}\neq 0$. The same inequality is the strong_cp_resolved field of the module certificate cpPhaseCert.
Framework reading: $\theta_{\mathrm{QCD}}$ is forced to zero by $J$-cost minimization (T5 uniqueness of $J$), while $\delta_{\mathrm{CKM}}$ is forced nonzero by Gray-code chirality and the directed eight-tick cycle (T7). There is therefore no fine-tuning: both outcomes are zero-parameter consequences of RCL plus $Q_3$ structure. The declaration closes the "energetic forcing" bullet in the module's main-results list (strong_cp_resolution).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.