berry_gen3
plain-language theorem explainer
Generation 3 (cube axis 2) accumulates Berry phase π/2 over one directed 8-tick Gray-code cycle. Anyone deriving δ_CKM from generation-dependent geometric phases cites this evaluation. The proof unfolds the phase-per-cycle definition and substitutes the Gray-code fact that bit 2 flips twice.
Claim. The discrete Berry phase accumulated by generation 3 (the eigenstate coupled to cube axis $2$) over one directed eight-tick Gray-code cycle equals $2 \cdot (\pi/4) = \pi/2$.
background
The module derives the CKM CP phase from Berry phases of generation eigenstates transported around the directed 8-tick Gray-code cycle on the recognition cube. For a discrete cycle the geometric phase is the sum of overlap arguments between consecutive states; here it collapses to a flip count times a fixed phase per flip.
berryPhasePerCycle g is defined as (bitFlipCount g) * phasePerFlip. The flip count is how many times bit g changes along the Gray-code edge list of the closed 8-tick path. Chirality of that path makes the three axes flip unequally: bit 0 four times, bit 2 twice (proved by bit2_flips_two). The per-flip phase is $\pi/4$, so generation 1 gets $\pi$ and generation 3 gets $\pi/2$.
Locally this sits under the distinction that $\theta_{\mathrm{QCD}}$ is energetic (driven to 0 by J-cost) while $\delta_{\mathrm{CKM}}$ is topological and can stay nonzero.
proof idea
Tactic proof in three steps. Unfold berryPhasePerCycle and phasePerFlip by simp only, leaving (bitFlipCount 2 : ℝ) * (π/4). Cast the natural-number identity bit2_flips_two : bitFlipCount 2 = 2 to reals, then rewrite. No further arithmetic is needed; the goal is exactly $2 \cdot (\pi/4)$.
why it matters
Fills the generation-3 slot in the Berry-phase table that feeds CP-phase assembly. The module formula is $\delta_{\mathrm{CKM}} = \gamma_{\mathrm{Berry}}(3) - \gamma_{\mathrm{Berry}}(2) - \gamma_{\mathrm{Berry}}(1)$ plus corrections; without unequal $\gamma$ values there is no CP violation from this mechanism. Sibling results berry_gen1, berry_gen2, and berryPhase_generation_dependent package the inequality; cp_phase_nonzero and cpPhaseRaw consume it.
Framework link: the directed Gray-code cycle is the eight-tick octave (T7) with chiral bit flips from the cube geometry (T8, $D=3$). Direction breaks T, so the geometric phase is a genuine weak-sector CP source while J-cost still forces $\theta_{\mathrm{QCD}}=0$. No downstream edges are recorded yet; the immediate consumers are the in-module CP-phase theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.