ValidTrajectory

formal source

  66/-! ## 8-tick trajectory structure -/
  67
  68/-- A valid 8-tick trajectory: 8 steps each in (ln φ)·ℤ that sum to zero. -/
  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) : ℤ :=
  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