phasePerFlip
plain-language theorem explainer
The elementary geometric phase step on the eight-tick Gray-code cycle is fixed at π/4. Anyone deriving generation-dependent Berry phases or the CKM CP angle from directed cube transport cites this constant. It is a one-line definition matching the discrete 8-tick phase ladder kπ/4.
Claim. The phase contribution of a single axis flip on the directed eight-tick cycle is $\pi/4$ (equivalently $2\pi/8$). For generation $k$, the total Berry phase per cycle is then $(\text{number of flips of axis }k)\times\pi/4$.
background
The module derives the CKM CP-violating phase $\delta_{\mathrm{CKM}}$ from Berry phases accumulated by generation eigenstates on the directed Gray-code 8-tick cycle. Transport around the cycle yields $$\gamma_{\mathrm{Berry}}(g)=\sum_{t=0}^{7}\arg\langle\psi_g(t)|\psi_g(t+1)\rangle,$$ and $\delta_{\mathrm{CKM}}$ is a signed combination of the three generation phases.
The eight-tick phase ladder (Foundation.EightTick) already sets discrete phases $k\pi/4$ for $k=0,\ldots,7$. A single bit flip advances one step on that ladder, so the elementary increment is $\pi/4$. Chirality of the Gray code makes different axes flip different numbers of times, so generations accumulate unequal phases; the directed cycle breaks time-reversal, leaving a topological CP phase while $\theta_{\mathrm{QCD}}$ is still driven to zero by $J$-cost.
proof idea
Pure definition: the real constant $\pi/4$ is assigned directly. No tactics or lemmas. The value is the unit step of the eight-tick phase function $\mathrm{phase}(k)=k\pi/4$, equivalently one eighth of a full $2\pi$ turn on the discrete cycle.
why it matters
This constant is the yardstick for all generation Berry phases in the module. berryPhasePerCycle multiplies flip counts by it; the three generation theorems then evaluate to $\pi$, $\pi/2$, and $\pi/2$ respectively, proving the phases are generation-dependent. That inequality, together with cycle direction, feeds the nonzero CP phase and the claim that $\delta_{\mathrm{CKM}}$ is topological while $\theta_{\mathrm{QCD}}$ is energetic. It sits on the T7 eight-tick octave: period $2^3$ forces the elementary angle $2\pi/8=\pi/4$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.