canonicalTrajectory
plain-language theorem explainer
CanonicalTrajectory supplies the minimal 8-tick sequence realizing any integer displacement n on the phi-lattice while enforcing sum-zero neutrality. Researchers closing Gap A in the GCIC paper cite this construction when deriving the discrete gauge r ~ r + n ln φ from T6 and T7. The definition proceeds by direct pattern matching on the tick index together with a one-line simp for the neutrality constraint.
Claim. For any integer $n$, the canonical trajectory is the ValidTrajectory whose steps assign $+n$ at tick 0, $-n$ at tick 1, and 0 for ticks 2 through 7, satisfying the neutrality condition that the sum of the eight steps equals zero.
background
ValidTrajectory is the structure of an 8-tuple of integers (each a multiple of ln φ) whose sum vanishes, directly encoding T7 neutrality. The GCIC Gap A module derives the discrete identification r ~ r + n ln φ from T6 (each step changes the log-ratio by an integer multiple of ln φ via φ-self-similarity) and T7 (sum of eight consecutive changes is zero). The module doc states that this upgrades the GCIC paper's explicit model input to a derived theorem, analogous to Bloch's theorem with the φ-lattice as periodic potential and the 8-tick period as crystal lattice.
proof idea
The definition uses pattern matching on the Fin 8 index to set steps 0 and 1 to n and -n with the rest zero; neutrality is discharged by a single simp [Fin.sum_univ_eight] application.
why it matters
This definition supplies the explicit witness used by eight_tick_compactification and discrete_gauge_forced, which establish that r ~ r + n ln φ is a dynamical equivalence forced by T6 + T7. It realizes the eight-tick octave (T7) and φ-self-similarity (T6) landmarks of the Recognition Science forcing chain, closing the acknowledged gap in the GCIC paper by making the compact phase a theorem rather than an input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.