ValidTrajectory
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not constrain individual step magnitudes beyond integrality.
- Does not enforce positivity or other physical selection rules on steps.
- Does not compute physical displacement; separate definitions handle that.
- Does not prove existence of trajectories for every integer displacement.
formal statement (Lean)
69structure ValidTrajectory where
70 /-- The 8 step sizes (integer multiples of ln φ). -/
71 steps : Fin 8 → ℤ
72 /-- T7: 8-tick neutrality - the steps sum to zero. -/
73 neutral : ∑ k : Fin 8, steps k = 0
74
75/-- Net displacement of a valid trajectory (in units of ln φ). -/
76def ValidTrajectory.netDisplacement (traj : ValidTrajectory) : ℤ :=
proof body
Definition body.
77 ∑ k : Fin 8, traj.steps k
78
79/-- Neutrality means net displacement is zero. -/
80theorem ValidTrajectory.net_zero (traj : ValidTrajectory) :
81 traj.netDisplacement = 0 :=
82 traj.neutral
83
84/-- Net physical displacement in ℝ. -/
85noncomputable def ValidTrajectory.netPhysical (traj : ValidTrajectory) : ℝ :=
86 ∑ k : Fin 8, (traj.steps k : ℝ) * Real.log phi
87
88/-- Net physical displacement is zero for a neutral trajectory. -/
89theorem ValidTrajectory.net_physical_zero (traj : ValidTrajectory) :
90 traj.netPhysical = 0 := by
91 unfold netPhysical
92 rw [← Finset.sum_mul]
93 have h : ∑ k : Fin 8, (traj.steps k : ℝ) = 0 := by
94 have := traj.neutral
95 exact_mod_cast this
96 rw [h, zero_mul]
97
98/-! ## The key theorem: any displacement is achievable -/
99
100/-- **CANONICAL 8-TICK TRAJECTORY FOR DISPLACEMENT n**
101
102 To achieve displacement n·ln φ in 8 ticks satisfying neutrality:
103 - Step 0: +n (forward)
104 - Step 1: -n (backward)
105 - Steps 2-7: 0
106
107 This is the simplest valid trajectory achieving any integer displacement n. -/