canonicalPath
plain-language theorem explainer
The canonical discrete transport path on the eight-vertex cube starts at a chosen vertex and advances by one step of the Gray-code cycle permutation at each tick. Anyone assembling Berry phases or the CKM CP phase from directed 8-tick transport cites this path as the geometric trajectory. It is a pure one-line definition: the k-fold iterate of the cycle map applied to the start vertex.
Claim. For each starting vertex $v \in \{0,\ldots,7\}$, the canonical transport path is the map sending tick $k$ to $\sigma^k(v)$, where $\sigma$ is the Gray-code cycle permutation on the eight cube vertices and $k$ runs through the eight ticks of the octave.
background
This module derives the CKM CP-violating phase $\delta_{\mathrm{CKM}}$ from the Berry phase accumulated by generation eigenstates as they traverse the directed 8-tick Gray-code cycle. The local geometric object is a discrete transport path: a map from the eight ticks to the eight cube vertices (one state per tick).
The cycle permutation $\sigma$ advances a vertex to the next vertex in the Gray-code order: if $v$ is visited at tick $t$, then $\sigma(v)$ is visited at tick $t+1$. Explicitly, $\sigma$ acts as $0\mapsto 1$, $1\mapsto 3$, $2\mapsto 6$, $3\mapsto 2$, $4\mapsto 0$, $5\mapsto 4$, $6\mapsto 7$, $7\mapsto 5$. The eight-tick period is the Recognition Science octave (forcing step T7).
The canonical path simply follows $\sigma$ from a fixed start: at tick $k$ the state is $\sigma^k(v)$. Downstream lemmas then show this path closes after eight steps and feed the discrete Berry-phase sum.
proof idea
Pure definition, not a proof. The body is the single term $\lambda k.,\sigma^{k}(v)$, i.e. the $k$-fold Function.iterate of the cycle permutation applied to the starting vertex. No lemmas are invoked at the definition site; closure and period facts appear only in the downstream theorem that uses this path.
why it matters
This path is the geometric carrier for the module's Berry-phase story. The immediate parent is the closure theorem: after eight ticks the path returns to its start (via the known period of the cycle permutation). That closed loop is what lets the discrete Berry phase $\gamma_{\mathrm{Berry}}(g)=\sum_{t=0}^{7}\arg\langle\psi_g(t)|\psi_g(t+1)\rangle$ be well-defined as a full-cycle geometric phase.
In the Recognition framework the directed Gray-code cycle is chiral and breaks time-reversal; generation-dependent coupling to the cube then makes $\gamma_{\mathrm{Berry}}$ generation-dependent, so the combination that defines $\delta_{\mathrm{CKM}}$ is nonzero. The same geometry underwrites the module's contrast with $\theta_{\mathrm{QCD}}$ (energetic, driven to zero by J-cost) versus $\delta_{\mathrm{CKM}}$ (topological, forced by the directed eight-tick octave). Without a named canonical path, the later nonzero-CP and T-violation statements have no concrete transport to evaluate on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.