cp_phase_positive
plain-language theorem explainer
The raw CP-violating phase built from generation Berry phases is strictly positive. Anyone packaging the CKM phase certificate or fixing the geometric sign convention against experiment would cite this. The proof unfolds the raw-phase definition, substitutes the first two generation Berry values, and closes by linear arithmetic from positivity of π.
Claim. The raw CP phase $\delta_{\mathrm{raw}}$, formed from the generation Berry phases on the directed eight-tick Gray-code cycle, satisfies $\delta_{\mathrm{raw}} > 0$.
background
This module extracts the CKM CP phase from geometric (Berry) phases accumulated by generation eigenstates as they traverse the directed 8-tick Gray-code cycle. For generation $g$,
$$\gamma_{\mathrm{Berry}}(g)=\sum_{t=0}^{7}\arg\langle\psi_g(t)|\psi_g(t+1)\rangle.$$
The raw CP phase is a fixed linear combination of these generation phases (schematically $\delta_{\mathrm{CKM}}=\gamma(3)-\gamma(2)-\gamma(1)$ plus corrections). The eight-tick phases themselves are the standard grid $k\pi/4$ for $k=0,\ldots,7$.
The local setting contrasts two CP-related quantities: $\theta_{\mathrm{QCD}}$ is energetic and driven to zero by J-cost minimization, while $\delta_{\mathrm{CKM}}$ is topological and forced nonzero by chirality of the directed Gray code together with generation-dependent coupling to the cube. Positivity of the raw phase is the sign half of that topological claim; nonvanishing is proved separately from chirality.
proof idea
Term-mode proof in three steps. Unfold the definition of the raw CP phase. Rewrite with the closed-form Berry values for generations 1 and 2 (berry_gen1, berry_gen2), which reduce the expression to an explicit real linear form in $\pi$. Finish by linarith using Real.pi_pos, so the reduced form is strictly positive.
why it matters
Feeds the CP-phase certificate cpPhaseCert, which packages nonvanishing, positivity, generation dependence, CPT preservation, and the strong-CP resolution ($\theta_{\mathrm{QCD}}=0$ by J-cost). Together with cp_phase_nonzero it supplies the sign-and-magnitude skeleton of $\delta_{\mathrm{CKM}}$ as a Berry-phase observable on the directed eight-tick cycle (forcing-chain T7).
The sign is convention-dependent in presentation but physical once the Gray-code orientation is fixed: reversing the cycle negates the Berry phase (T violation with CPT intact). That is the geometric counterpart of weak-sector CP violation while the energetic Strong-CP angle remains zero. Downstream certificate consumers treat positivity as a checked field rather than an open hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.