cp_phase_changes_sign_under_reversal
plain-language theorem explainer
Cycle reversal sends the raw CP phase to its negative: if the forward Gray-code loop yields δ_raw from generation Berry phases, the backward loop yields −δ_raw. Anyone tracking T-odd structure of δ_CKM or CPT balance in the RS weak sector would cite this. The proof is a pure algebraic identity: unfold the raw-phase definition and close by ring.
Claim. Let $\delta_{\mathrm{raw}}$ be the raw CP phase built from per-cycle Berry phases of generation eigenstates, and write $\gamma_g$ for the Berry phase of generation $g$ around the directed 8-tick cycle. Then $-\delta_{\mathrm{raw}} = -(\gamma_0 - \gamma_1)$. Equivalently, reversing the cycle direction negates the CP phase extracted from those Berry phases.
background
This module extracts the CKM CP phase from geometric (Berry) phases accumulated by generation eigenstates transported around the directed 8-tick Gray-code cycle on the recognition cube. For a discrete loop the Berry phase of generation $g$ is
$$\gamma_g = \sum_{t=0}^{7} \arg\langle\psi_g(t)\mid\psi_g(t+1)\rangle,$$
the argument of the product of consecutive overlaps. The raw CP combination is a signed difference of these generation phases (here generations 0 and 1); the physical $\delta_{\mathrm{CKM}}$ is that combination plus higher-generation corrections.
The eight-tick register supplies the discrete phases $k\pi/4$ for $k=0,\ldots,7$, and the Gray-code orientation is chiral: different axes flip different numbers of times, so directed traversal breaks time-reversal. The module's standing distinction is that $\theta_{\mathrm{QCD}}$ is an energetic J-cost parameter driven to zero, while $\delta_{\mathrm{CKM}}$ is topological and can stay nonzero.
Sibling facts already record that Berry phases depend on generation and that the raw CP phase is nonzero from chirality. The present claim isolates the sign response under orientation reversal.
proof idea
Term-mode tactic proof, two steps. First unfold cpPhaseRaw replaces the raw CP phase by its defining combination of per-cycle Berry phases (the difference $\gamma_0-\gamma_1$). Second ring closes the purely algebraic identity $-\delta_{\mathrm{raw}} = -(\gamma_0-\gamma_1)$. No external lemmas are invoked; the content is definitional plus commutative-ring normalization.
why it matters
Listed among the module's main results as the T-violation companion to cp_phase_nonzero: forward chirality produces a nonzero CP phase, and reversing the cycle flips its sign. That sign flip is exactly the T-odd response expected of a directed Berry phase (each overlap $\langle\psi(t)\mid\psi(t+1)\rangle$ conjugates to $\langle\psi(t+1)\mid\psi(t)\rangle$, negating the phase). The immediately following CPT comment records the intended balance: CP violation from forward chirality cancels T violation from backward chirality in the total phase product.
Framework landmarks: the underlying loop is the T7 eight-tick octave; the Gray-code chirality that makes $\gamma_g$ generation-dependent is the same directed structure used in CKM-from-cube constructions. The claim sharpens the module's Strong-CP resolution story without touching the J-cost minimization of $\theta_{\mathrm{QCD}}$. No downstream users are wired yet; the natural parents are a CPT-preservation statement and any numerical assembly of $\delta_{\mathrm{CKM}}$ that must track orientation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.