cpPhaseRaw
plain-language theorem explainer
Raw CP-violating phase is the difference of generation-1 and generation-2 Berry phases on the directed eight-tick Gray-code cycle, equaling π/2 in the discrete model. Anyone deriving δ_CKM, the Jarlskog invariant, or the strong-CP split cites this quantity. It is a one-line difference of two already-defined per-cycle Berry phases.
Claim. Define the raw CP phase by $\delta_{\mathrm{raw}} := \gamma(0) - \gamma(1)$, where $\gamma(g)$ is the total Berry phase accumulated by generation $g$ over one directed eight-tick cycle. In the discrete model this evaluates to $\pi - \pi/2 = \pi/2$.
background
The module derives the CKM CP 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 overlap arguments between consecutive states; here it collapses to a count of bit flips on the generation axis times a fixed phase per flip.
Upstream, berryPhasePerCycle g is (bitFlipCount g) * phasePerFlip, and the eight-tick phases are $k\pi/4$ for $k=0,\ldots,7$. Generation 1 (axis 0) therefore gets $\gamma=4\cdot\pi/4=\pi$; generation 2 gets $\pi/2$. The module stresses the split: $\theta_{\mathrm{QCD}}$ is energetic and driven to zero by J-cost, while $\delta_{\mathrm{CKM}}$ is topological and forced nonzero by chirality of the directed cycle (T7 eight-tick octave, Gray-code chirality).
proof idea
Pure definition: unfold to the difference of the two generation Berry phases already defined by berryPhasePerCycle. No tactics. Downstream lemmas (cp_phase_nonzero, cp_phase_positive) then rewrite with the closed forms berry_gen1 and berry_gen2 and finish by linarith against Real.pi_pos.
why it matters
This is the numeric carrier for weak-sector CP violation in the RS Standard Model stack. It feeds cp_phase_nonzero and cp_phase_positive (the fundamental claim that Gray-code chirality forces $\delta\neq 0$), the sign-reversal and CPT identities, and the certificate CPPhaseCert. It also supplies cpAngle and cp_small_but_nonzero in the Jarlskog module.
Together with the J-cost minimum for $\theta_{\mathrm{QCD}}$, it underwrites strong_cp_resolved_with_ckm_cp: energetic forcing of strong CP to zero while topological Berry geometry keeps CKM CP nonzero. That is the module's resolution of the strong-CP problem without killing weak CP. Framework landmarks: T7 eight-tick cycle, directed Gray-code chirality, and the energetic-vs-topological split stated in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.