discrete_gauge_forced
plain-language theorem explainer
The discrete gauge theorem shows that for any real r1 and integer n there exists a valid 8-tick trajectory whose first step displaces the log-ratio by exactly n ln φ, making r and r + n ln φ dynamically equivalent. Researchers closing gaps in the GCIC paper would cite this to replace an explicit model input with a derived consequence of T6 and T7. The proof is a one-line wrapper that constructs the trajectory via canonicalTrajectory n and simplifies the displacement equality.
Claim. For all real numbers $r_1$ and integers $n$, there exists a valid 8-tick trajectory $traj$ such that $r_1 + (traj.steps(0) : ℝ) · ln φ = r_1 + n · ln φ$.
background
The GCIC module formalizes Mechanism A from the GCIC Response paper: 8-tick neutrality plus φ-self-similarity forces the discrete gauge r ~ r + n ln φ. A ValidTrajectory is a structure whose steps : Fin 8 → ℤ sum to zero, encoding T7 neutrality while each step is an integer multiple of ln φ by T6. The local setting derives the compact phase Θ = r / ln φ mod 1 as a Bloch-like consequence of the φ-lattice and 8-tick crystal period, without imposing periodicity by hand.
proof idea
This is a one-line wrapper that applies the canonicalTrajectory construction for the given n and uses simp on the canonicalTrajectory definition to confirm the first-step displacement equals n ln φ.
why it matters
This theorem discharges the acknowledged gap in the GCIC Response paper by deriving the discrete identification from T6 (φ-step) and T7 (8-tick neutrality) rather than treating it as an explicit model input. It directly supports the compactPhase and compactPhase_gauge_invariant definitions in the same module and aligns with the eight-tick octave and φ-ladder landmarks in the Recognition Science forcing chain. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.