berry_gen1
plain-language theorem explainer
Generation 1 (axis 0) accumulates Berry phase π over one directed eight-tick Gray-code cycle: four bit flips times π/4 per flip. Anyone deriving δ_CKM or the Jarlskog invariant from cube chirality cites this evaluation. The proof is a short rewrite that inserts the known flip count for bit 0.
Claim. The Berry phase accumulated by generation 1 (axis $0$) over one directed eight-tick cycle equals $4\cdot(\pi/4)$, hence $\pi$.
background
This module extracts the CKM CP phase from geometric (Berry) phases that generation eigenstates pick up while traversing the directed Gray-code cycle on the three-bit cube. For a discrete eight-tick loop the phase is the sum of overlap arguments between consecutive states; in the RS setup it factors as (number of flips of the generation's axis) times a fixed phase per flip of $\pi/4$.
The eight-tick phases themselves are the standard ladder $k\pi/4$ for $k=0,\ldots,7$. Chirality of the Gray code is recorded by bitFlipCount: how many times each cube axis flips during one full cycle. Upstream, bit 0 is known to flip exactly four times (bit0_flips_four). Generation labels identify which axis a given fermion generation couples to; generation 1 is axis 0.
The local claim is therefore purely combinatorial: plug the flip count for axis 0 into the per-cycle Berry-phase formula.
proof idea
Unfold the definitions of Berry phase per cycle and phase per flip. The goal reduces to showing that the real cast of the flip count for bit 0 equals 4. That equality is bit0_flips_four (proved by native_decide on the Gray-code flip list), cast to $\mathbb{R}$, then rewritten into the goal. No analytic estimates are required.
why it matters
This is the generation-1 anchor in the CP-phase chain. Downstream, berryPhase_generation_dependent rewrites both generation-1 and generation-2 evaluations and uses $\pi>0$ to show the phases differ, a necessary condition for CP violation. The same two rewrites discharge cp_phase_nonzero and cp_phase_positive for the raw CP combination. Farther downstream, Jarlskog results (sin_cp_angle_nonzero, jarlskog_positive, cp_small_but_nonzero) inherit the concrete value $\pi/2$ for the structural CP angle once generation 1 contributes $\pi$ and generation 2 contributes $\pi/2$.
Framework-wise this sits on the eight-tick octave (T7) and the chiral Gray-code geometry of the cube: $\delta_{\mathrm{CKM}}$ is topological (Berry), while $\theta_{\mathrm{QCD}}$ is energetic and driven to zero by J-cost, resolving Strong CP without killing weak CP violation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.