strong_cp_resolved_with_ckm_cp
plain-language theorem explainer
The Strong CP problem is resolved by pairing two facts: the QCD vacuum angle is forced to zero as the unique J-cost minimum, while the CKM CP phase is forced nonzero by Gray-code chirality. Anyone citing the RS split between energetic θ_QCD and topological δ_CKM would use this certificate. The proof is a one-line pairing of the cost-minimization lemma with the nonzero Berry-phase difference.
Claim. For every real angle $\theta$, $0 \leq 1 - \cos\theta$, and the raw CKM CP phase $\delta_{\mathrm{raw}} = \gamma_{\mathrm{Berry}}(1) - \gamma_{\mathrm{Berry}}(2)$ is nonzero.
background
In this module the CKM CP phase is derived from Berry phases of generation eigenstates transported around the directed 8-tick Gray-code cycle on the cube $Q_3$. The discrete Berry phase is the argument sum of consecutive overlaps; different generations couple to different cube levels, so the phases differ. The raw CP phase is their difference, $\delta_{\mathrm{raw}} = \gamma(0) - \gamma(1)$, which evaluates to $\pi/2$.
The Strong CP angle is treated separately. The QCD vacuum is parametrized by $\theta \in [0,2\pi)$ with effective cost $J_{\mathrm{eff}}(\theta) = J_0 + \Delta(1-\cos\theta)$, $\Delta>0$. Because $\cos\theta \le 1$, any nonzero $\theta$ raises the cost, so the minimum sits at $\theta=0$.
Upstream, theta_qcd_cost_minimized_at_zero is exactly $\forall\theta,,0\le 1-\cos\theta$. Upstream cp_phase_nonzero unfolds the raw phase to generation Berry values and obtains a contradiction from $\pi>0$ if the difference vanished. The module doc stresses the split: $\theta_{\mathrm{QCD}}$ is energetic, $\delta_{\mathrm{CKM}}$ is topological.
proof idea
Term-mode one-liner. The goal is a conjunction; the proof applies the pair constructor to the two already-proved conjuncts theta_qcd_cost_minimized_at_zero and cp_phase_nonzero. No rewriting, unfolding, or arithmetic is performed at this site.
why it matters
This is the module's explicit Strong-CP resolution certificate. The doc-comment states there is no fine-tuning: $\theta_{\mathrm{QCD}}$ is energetically forced to 0 by J-cost, while $\delta_{\mathrm{CKM}}$ is geometrically forced nonzero by Gray-code chirality, both zero-parameter consequences of RCL plus $Q_3$. The J-cost side sits on T5 J-uniqueness and the Recognition Composition Law; the CP side uses the eight-tick octave (T7) and directed cycle chirality that breaks time-reversal. No used_by edges are recorded yet; the theorem stands as the capstone pairing of the two main results listed in the module doc (cp_phase_nonzero and the $\theta_{\mathrm{QCD}}$ cost minimum).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.