  47/-! ## The lattice of accessible displacements -/
  48
  49/-- A valid single-step displacement: an integer multiple of ln φ. -/
  50def ValidStep (delta : ℝ) : Prop :=
  51  ∃ n : ℤ, delta = n * Real.log phi
  52
  53/-- ln φ is positive. -/
  54lemma log_phi_pos : 0 < Real.log phi := by
  55  exact Real.log_pos one_lt_phi
  56
  57/-- ln φ ≠ 0. -/
  58lemma log_phi_ne_zero : Real.log phi ≠ 0 :=
  59  ne_of_gt log_phi_pos
  60
  61/-- n·ln φ is a valid step for any integer n. -/
  62lemma int_mul_log_phi_valid_step (n : ℤ) :
  63    ValidStep (n * Real.log phi) :=
  64  ⟨n, rfl⟩
  65
  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) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.