berryPhasePerCycle
plain-language theorem explainer
Defines the discrete Berry phase accumulated by generation axis g over one directed 8-tick Gray-code cycle: flip count of that axis times π/4. Anyone deriving δ_CKM from cube chirality cites this as the per-generation geometric phase. The body is a one-line product of the Gray-code flip tally and the fixed phase-per-flip quantum.
Claim. For each generation axis $g \in \{0,1,2\}$, the Berry phase per directed 8-tick cycle is $\gamma_{\mathrm{Berry}}(g) = N_{\mathrm{flip}}(g)\,\cdot\,\pi/4$, where $N_{\mathrm{flip}}(g)$ is the number of times bit $g$ flips on the Gray-code cycle and $\pi/4$ is the phase increment per flip.
background
The module derives the CKM CP phase from geometric (Berry) phase picked up by generation eigenstates as they traverse the directed 8-tick Gray-code cycle on the recognition cube. The discrete sum $\gamma_{\mathrm{Berry}}(g)=\sum_t\arg\langle\psi_g(t)|\psi_g(t+1)\rangle$ collapses, for this transport, to a count of axis flips times a fixed phase quantum.
Upstream, phase on the eight-tick ladder is $k\pi/4$ for $k=0,\ldots,7$, so one step contributes $\pi/4$. The sibling constant phase-per-flip is exactly that quantum: each flip of axis $k$ adds $\pi/4$ to generation $k$'s Berry phase. Gray-code chirality supplies the flip tally $N_{\mathrm{flip}}(g)$ (bit 0 flips four times; bits 1 and 2 flip twice). Generations are the three cube axes (Fin 3), matching the three fermion generations.
Local setting: $\theta_{\mathrm{QCD}}$ is energetic and driven to zero by J-cost, while $\delta_{\mathrm{CKM}}$ is topological and comes from this directed Berry geometry.
proof idea
Pure definition: cast the natural-number flip count of axis $g$ to $\mathbb{R}$ and multiply by the constant phase-per-flip $\pi/4$. No tactics; the mathematical content is the product of those two upstream quantities.
why it matters
This is the generation-resolved geometric phase that feeds the whole CP-phase derivation. Immediate parents evaluate it on each axis: generation 0 gets $4\cdot\pi/4=\pi$; generations 1 and 2 get $2\cdot\pi/4=\pi/2$. Those values prove the phases are generation-dependent (necessary for CP violation), enter the raw CP combination $\mathrm{cpPhaseRaw}$, the sign-reversal identity under cycle reversal (T violation with CPT preserved), and the CPPhaseCert bundle. Downstream Jarlskog work uses the same phase to show $\sin\delta\neq 0$.
Framework landmarks: the eight-tick octave (T7) supplies the cycle and the $\pi/4$ quantum; Gray-code chirality on the $D=3$ cube (T8) makes flip counts unequal across axes. That inequality is why $\delta_{\mathrm{CKM}}$ is nonzero while Strong CP remains resolved by J-cost minimization of $\theta_{\mathrm{QCD}}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.