sync_exceeds_both

formal source

  47  exact syncPeriod_3
  48
  49/-- The sync period is strictly greater than either individual period. -/
  50theorem sync_exceeds_both :
  51    gap45.sync_period > gap45.recognition_period ∧
  52    gap45.sync_period > gap45.phase_period := by
  53  constructor <;> simp [gap45, Gap45Frustration.sync_period,
  54    Gap45Frustration.recognition_period, Gap45Frustration.phase_period,
  55    syncPeriod_3]
  56  all_goals norm_num
  57
  58/-! ## The Perpetual Complexity Theorem -/
  59
  60/-- At every 360-tick boundary, there exist voxels where the recognition
  61    and phase cadences are misaligned. These voxels have positive local
  62    J-cost (they are not at x=1) and constitute structured excitations. -/
  63structure MisalignmentWitness where
  64  tick : ℕ
  65  misaligned : tick % 8 ≠ 0 ∨ tick % 45 ≠ 0
  66
  67/-- For any tick that is not a multiple of lcm(8,45) = 360, at least
  68    one cadence is not at its period boundary. -/
  69theorem misalignment_exists (t : ℕ) (h : t % 360 ≠ 0) :
  70    t % 8 ≠ 0 ∨ t % 45 ≠ 0 := by
  71  by_contra h_neg
  72  push_neg at h_neg
  73  obtain ⟨h8, h45⟩ := h_neg
  74  have : 360 ∣ t := by
  75    have := Nat.Coprime.mul_dvd_of_dvd_of_dvd (by native_decide : Nat.Coprime 8 45)
  76      (Nat.dvd_of_mod_eq_zero h8) (Nat.dvd_of_mod_eq_zero h45)
  77    simpa using this
  78  exact h (Nat.mod_eq_zero_of_dvd this)
  79
  80/-- Between any two multiples of 360, there are 359 misaligned ticks. -/