ValidTrajectory
plain-language theorem explainer
ValidTrajectory packages an 8-step sequence of integer multiples of ln φ whose total sum vanishes, implementing the neutrality condition of T7. Researchers deriving discrete gauge identifications from the Recognition Science forcing chain cite this structure when constructing trajectories that realize compactification of the log-ratio variable. The definition is a direct record of the two fields required by the 8-tick neutrality condition.
Claim. A structure consisting of a map $steps : Fin 8 → ℤ$ together with the condition that $∑_{k=0}^7 steps(k) = 0$.
background
In the GCIC module this structure formalizes valid 8-tick trajectories under the two forcing results T6 (φ-self-similarity forces each Δr_k to lie in (ln φ)·ℤ) and T7 (the sum of eight consecutive changes vanishes). The module doc states that these two results together derive the discrete identification r ~ r + n·ln φ as a dynamical consequence rather than an imposed input. Upstream, the tick constant supplies the fundamental time quantum while the phi constant supplies the self-similar fixed point used to scale the steps.
proof idea
This declaration is a structure definition that directly records the steps function and the neutrality sum condition. No lemmas or tactics are invoked; the type serves as the carrier for later constructions such as canonicalTrajectory.
why it matters
The structure supplies the carrier type for canonicalTrajectory, canonicalTrajectory_net_zero, eight_tick_compactification and discrete_gauge_forced. Those results close the acknowledged gap in the GCIC paper by showing that the discrete gauge r ~ r + n·ln φ follows from T6 + T7. It thereby realizes the eight-tick octave (T7) as the mechanism that compactifies the phi-lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.