cp_phase_nonzero
plain-language theorem explainer
The raw CKM CP phase, defined as the difference of generation-1 and generation-2 Berry phases on the directed eight-tick Gray-code cycle, is nonzero. Anyone deriving weak CP violation or the Strong-CP resolution from Recognition geometry cites this. The proof substitutes the closed-form Berry phases π and π/2 and uses positivity of π.
Claim. The raw CP phase $\delta_{\mathrm{raw}} := \gamma_{\mathrm{Berry}}(1) - \gamma_{\mathrm{Berry}}(2)$ satisfies $\delta_{\mathrm{raw}} \neq 0$, where $\gamma_{\mathrm{Berry}}(g)$ is the discrete Berry phase accumulated by generation $g$ over one directed eight-tick Gray-code cycle.
background
This module extracts the CKM CP-violating phase from geometric (Berry) phases of generation eigenstates transported around the directed 8-tick Gray-code cycle. For a discrete cycle the Berry phase is the sum of consecutive overlap arguments; here it reduces to (number of axis flips) times the elementary phase $\pi/4$ from the eight-tick phase ladder $k\pi/4$.
Generation 1 (axis 0) flips four times per cycle, so $\gamma(1)=\pi$. Generation 2 (axis 1) flips twice, so $\gamma(2)=\pi/2$. The raw CP phase is their difference $\delta_{\mathrm{raw}}=\gamma(1)-\gamma(2)$. Chirality of the Gray code (unequal flip counts across axes) makes the generations inequivalent; the directed traversal breaks time-reversal symmetry.
The module contrasts this topological $\delta_{\mathrm{CKM}}$ with the energetic QCD angle $\theta_{\mathrm{QCD}}$, which J-cost minimization forces to zero. That split is the Recognition account of Strong CP versus weak CP violation.
proof idea
Unfold the definition of the raw CP phase to $\gamma(0)-\gamma(1)$. Rewrite with the two closed-form evaluations: generation-1 Berry phase equals $4\cdot(\pi/4)$ and generation-2 equals $2\cdot(\pi/4)$. The goal becomes $\pi-\pi/2\neq 0$. Assume equality to zero and discharge by linear arithmetic using positivity of $\pi$. No further geometric lemmas are needed once the flip-count identities are in place.
why it matters
This is listed among the module's main results as the fundamental nonzero-CP statement: CP is violated because the Gray-code cycle is chiral. It is the second conjunct of strong_cp_resolved_with_ckm_cp, which packages $\theta_{\mathrm{QCD}}=0$ (unique J-cost minimum) together with $\delta_{\mathrm{raw}}\neq 0$ (topologically protected). It also fills the cp_nonzero field of the CP-phase certificate.
In the broader framework it sits on the eight-tick octave (T7) and the directed Gray-code geometry: unequal axis flip counts force generation-dependent Berry phases, hence a nonzero weak CP phase, while J-cost still kills the strong angle. No free parameter is tuned on either side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.