beat_diff

formal source

  37theorem coprime_barrier : Nat.Coprime 8 45 := by native_decide
  38
  39/-- 37 = 45 - 8. The "beat" between the two periods. -/
  40theorem beat_diff : 45 - 8 = 37 := by norm_num
  41
  42/-- 37 is prime: the beat frequency is irreducible. -/
  43theorem beat_is_prime : Nat.Prime 37 := by native_decide
  44
  45/-- gcd(37, 360) = 1: the beat frequency 37/360 is in lowest terms. -/
  46theorem beat_fraction_irreducible : Nat.gcd 37 360 = 1 := by native_decide
  47
  48/-! ## Window Insufficiency -/
  49
  50/-- No window of length w < 360 can simultaneously be a multiple of 8 and 45.
  51    Any finite-horizon procedure with horizon < 360 ticks will encounter a tick
  52    where it cannot verify alignment of both periods. -/
  53theorem window_insufficient (w : ℕ) (hw_pos : 0 < w) (hw_lt : w < 360) :
  54    ¬ (8 ∣ w ∧ 45 ∣ w) :=
  55  IndisputableMonolith.Gap45.Beat.no_smaller_multiple_8_45 hw_pos hw_lt
  56
  57/-- The minimal window that resolves both periodicities is exactly 360. -/
  58theorem minimal_resolution_window : 8 ∣ 360 ∧ 45 ∣ 360 := by
  59  exact ⟨⟨45, by norm_num⟩, ⟨8, by norm_num⟩⟩
  60
  61/-- Any window resolving both periodicities must be ≥ 360. -/
  62theorem resolution_requires_full_period (w : ℕ) (h8 : 8 ∣ w) (h45 : 45 ∣ w) :
  63    360 ∣ w :=
  64  IndisputableMonolith.Gap45.Beat.minimal_sync_360_divides h8 h45
  65
  66/-! ## Aliasing: Why Experience Feels Continuous -/
  67
  68/-- The aliasing ratio: 37/45 < 1.
  69    Because the beat frequency (37 ticks per 45-fold cycle) is less than
  70    one full cycle, discrete ticks alias into apparent continuity.