berry_gen2
plain-language theorem explainer
Generation 2 (Gray-code axis 1) accumulates Berry phase $2\cdot\pi/4=\pi/2$ on one directed 8-tick cycle, because that axis flips twice. Anyone deriving $\delta_{\mathrm{CKM}}$ or the Jarlskog sign from generation-dependent geometric phases cites this evaluation. The proof unfolds the phase-per-cycle definition and rewrites with the bit-1 flip count.
Claim. The discrete Berry phase accumulated by generation 2 (the eigenstate coupled to Gray-code axis $1$) over one directed eight-tick cycle equals $2\cdot(\pi/4)$. Equivalently, if each bit flip contributes phase $\pi/4$, then axis $1$ contributes exactly twice that amount.
background
This module builds $\delta_{\mathrm{CKM}}$ from geometric phases of generation eigenstates transported around the directed Gray-code 8-tick cycle. The discrete Berry phase is the sum of overlap arguments along consecutive ticks; for the cube cycle it reduces to (number of flips of the generation's axis) times a fixed phase per flip.
bitFlipCount counts how often each of the three cube bits flips on the standard 8-tick Gray path. Chirality of that path is the fact that the three axes flip unequally: bit 0 flips four times, bits 1 and 2 flip twice each (bit1_flips_two). The local phase quantum is the eight-tick phase step $\pi/4$ from the EightTick ladder.
phasePerFlip packages that step; berryPhasePerCycle g is then bitFlipCount g times phasePerFlip. Generation labels here are the three cube axes (Fin 3), matching the three fermion generations in the RS ledger.
proof idea
Tactic proof in three steps. First simp only [berryPhasePerCycle, phasePerFlip] expands the left-hand side to the product of the real-cast flip count for bit 1 with $\pi/4$. Second, exact_mod_cast bit1_flips_two supplies (bitFlipCount 1 : $\mathbb{R}$) = 2. Third, rewrite by that equality yields $2\cdot(\pi/4)$. No analysis beyond the already-decided Gray-code flip census.
why it matters
Closes the generation-2 slot in the Berry-phase table used for CP. Downstream, berryPhase_generation_dependent rewrites with berry_gen1 and berry_gen2 to get $\pi\neq\pi/2$, the necessary inequality for a nonzero CP combination. The same two evaluations feed cp_phase_nonzero and cp_phase_positive on the raw CP combination, and thence Jarlskog positivity, sin_cp_angle_nonzero, and cp_small_but_nonzero.
In the module narrative this is the topological half of the Strong-CP resolution: $\theta_{\mathrm{QCD}}$ is driven to zero by J-cost, while $\delta_{\mathrm{CKM}}$ stays nonzero because the directed Gray cycle is chiral (T7 eight-tick octave, cube axes). Without the explicit $\pi/2$ value for axis 1, the difference that becomes $\delta$ cannot be shown positive or nonzero in Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.