eight_tick_compactification
plain-language theorem explainer
The theorem shows that for any real r₀ and integer n there exists a valid 8-tick trajectory whose first step displaces the log-ratio by exactly n ln φ. Researchers closing the discrete-gauge gap in the GCIC paper or deriving dynamical equivalences in Recognition Science would cite it. The proof is a one-line term wrapper that instantiates canonicalTrajectory n and simplifies the step value.
Claim. For any real number $r_0$ and integer $n$, there exists a valid 8-tick trajectory $τ$ (eight integer steps summing to zero) such that $r_0 + τ.steps(0) · ln φ = r_0 + n · ln φ$.
background
The module derives the discrete gauge r ~ r + n ln φ as a dynamical consequence rather than an input. A valid 8-tick trajectory is a Fin 8 → ℤ structure whose entries are the step sizes in units of ln φ and whose sum is zero (T7 neutrality). This rests on T6, which forces each individual step to be an integer multiple of ln φ by φ-self-similarity (φ² = φ + 1). The local setting is Mechanism A of the GCIC Response paper, which upgrades the identification from an explicit model assumption to a theorem derived from the forcing chain.
proof idea
The proof is a one-line term-mode wrapper. It applies the canonicalTrajectory constructor to the supplied integer n, then uses simp on the canonicalTrajectory definition to confirm that the zeroth step equals n and thereby satisfies the displacement equation.
why it matters
This declaration discharges Gap A of the GCIC paper by showing the discrete identification r ~ r + n ln φ is forced by T6 (φ-step) plus T7 (eight-tick neutrality). It supplies the direct analog of Bloch's theorem for the φ-lattice and supports the eight-tick octave in the Recognition framework. The result enables the remaining gauge-invariant constructions in the module (compactPhase, discrete_gauge_forced) without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.