berryPhase_generation_dependent
plain-language theorem explainer
Generation eigenstates pick up unequal Berry phases on one directed eight-tick Gray-code cycle. Anyone building δ_CKM from geometric phase cites this inequality as the necessary condition for weak CP violation. The proof rewrites the two phases to explicit multiples of π and contradicts π > 0.
Claim. The discrete Berry phase accumulated over one directed eight-tick cycle by generation $0$ is unequal to that of generation $1$: $\gamma_{\mathrm{Berry}}(0)\neq\gamma_{\mathrm{Berry}}(1)$.
background
This module derives the CKM CP phase from geometric phase on the directed 8-tick Gray-code cycle. A generation eigenstate $|\psi_g\rangle$ transported around the cycle accumulates
$$\gamma_{\mathrm{Berry}}(g)=\sum_{t=0}^{7}\arg\langle\psi_g(t)|\psi_g(t+1)\rangle.$$
In the discrete setting this is the argument of the product of consecutive overlap phases. The eight-tick phases themselves are the standard grid $k\pi/4$ for $k=0,\ldots,7$ (Foundation.EightTick).
Different generations couple to different CW levels of the cube $Q_3$, and the Gray code is chiral: axes flip unequal numbers of times. Directed traversal therefore breaks time-reversal symmetry, so the per-cycle Berry phases need not coincide. The module contrasts this topological $\delta_{\mathrm{CKM}}$ with $\theta_{\mathrm{QCD}}$, which is energetic and driven to zero by J-cost minimization.
proof idea
Term-mode proof by direct evaluation. Rewrite the two sides with the closed-form lemmas for generation-1 and generation-2 Berry phases (siblings that fix $\gamma$ to explicit multiples of $\pi$, classically $\pi$ and $\pi/2$). Assume equality, then linarith with Real.pi_pos yields the contradiction. No cycle geometry is re-proved here; the work is already in those evaluation lemmas.
why it matters
Listed among the module's main results as the generation-dependence step that makes CP violation possible. Downstream it is wired into cpPhaseCert as the generation_dependent field, alongside cp_phase_nonzero, positivity, CPT preservation, and the Strong-CP resolution $\theta_{\mathrm{QCD}}=0$.
Framework role: the eight-tick octave (T7) and Gray-code chirality supply a topological, directed phase that is generation-dependent, while J-cost still forces the Strong-CP angle to vanish. That split (topological weak CP vs energetic Strong CP) is the module's central claim. The raw CP phase is then the difference of these Berry phases, classically $\pi/2$, feeding the nonzero certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.