canonical_path_closed
plain-language theorem explainer
The canonical Gray-code transport path on the eight cube vertices, evaluated at tick 0, equals eight applications of the cycle permutation. Anyone setting up a discrete Berry phase for generation eigenstates on the directed 8-tick cycle needs this closed-loop identity. The proof unfolds the path at zero iterates to the identity and invokes the period-8 theorem for the cycle map.
Claim. For every vertex $v\in\{0,\ldots,7\}$, the canonical transport path based at $v$, evaluated at tick $0$, equals the eighth iterate of the Gray-code cycle permutation: $\mathrm{path}_v(0)=\sigma^8(v)$. Equivalently, since $\sigma$ has period $8$, the path at tick $0$ returns the base vertex $v$.
background
This module derives the CKM CP phase $\delta_{\mathrm{CKM}}$ from the Berry phase accumulated by generation eigenstates transported around the directed 8-tick Gray-code cycle on the cube vertices $\mathrm{Fin},8$. The geometric phase is the cycle sum
$$\gamma_{\mathrm{Berry}}(g)=\sum_{t=0}^{7}\arg\langle\psi_g(t)\mid\psi_g(t+1)\rangle,$$
and $\delta_{\mathrm{CKM}}$ is a fixed integer combination of the three generation phases.
The one-step advance is the cycle permutation $\sigma$: if $v$ is visited at tick $t$, then $\sigma(v)$ is the vertex at tick $t+1$ (explicitly $0\mapsto 1\mapsto 3\mapsto 2\mapsto 6\mapsto 7\mapsto 5\mapsto 4\mapsto 0$). Upstream, cyclePerm_period states that $\sigma$ has period exactly eight: $(\sigma^8)(v)=v$ for every $v$. That period is the T7 eight-tick octave of the forcing chain. A path that closes under this period is the minimal geometric input before a Berry phase is a true cycle holonomy rather than an open-path phase.
proof idea
Short term proof. Unfolding the canonical path at the zero tick index, together with Function.iterate_zero and the identity map, reduces the left-hand side to $v$. The upstream period theorem then gives $(\sigma^8)(v)=v$; taking the symmetric form of that equality matches the two sides. No case split on vertices is needed here: the period result already discharges all eight points by fin_cases and native_decide upstream.
why it matters
Path closure is the geometric prerequisite for every Berry-phase claim in the module: generation phases, their mutual differences, and the nonzero CP combination built from chirality of the directed Gray code. The module's Strong-CP resolution rests on the split that $\theta_{\mathrm{QCD}}$ is energetic (driven to zero by $J$-cost minimization) while $\delta_{\mathrm{CKM}}$ is topological (a nonzero Berry phase from directed chiral transport). This lemma pins the topological side to the T7 eight-tick octave and to the cycle operator from Foundation.CycleOperator. No downstream edges are recorded yet; natural consumers are the sibling return, per-cycle Berry, and cp_phase_nonzero results in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.