IndisputableMonolith.Streams

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4
   5/-! #### Streams: periodic extension and finite sums -/
   6namespace Streams
   7
   8open Classical
   9
  10/-- Boolean stream as an infinite display. -/
  11def Stream := Nat → Bool
  12
  13/-- A finite window/pattern of length `n`. -/
  14def Pattern (n : Nat) := Fin n → Bool
  15
  16/-- Integer functional `Z` counting ones in a finite window. -/
  17def Z_of_window {n : Nat} (w : Pattern n) : Nat :=
  18  ∑ i : Fin n, (if w i then 1 else 0)
  19
  20lemma Z_of_window_nonneg {n : Nat} (w : Pattern n) : 0 ≤ Z_of_window w := by
  21  unfold Z_of_window
  22  apply Finset.sum_nonneg
  23  intro i _
  24  split <;> decide
  25
  26@[simp] lemma Z_of_window_zero (w : Pattern 0) : Z_of_window w = 0 := by
  27  simp [Z_of_window]
  28
  29/-- The cylinder set of streams whose first `n` bits coincide with the window `w`. -/
  30def Cylinder {n : Nat} (w : Pattern n) : Set Stream :=
  31  { s | ∀ i : Fin n, s i.val = w i }
  32
  33@[simp] lemma mem_Cylinder_zero (w : Pattern 0) (s : Stream) : s ∈ Cylinder w := by
  34  intro i; exact (Fin.elim0 i)
  35
  36@[simp] lemma Cylinder_zero (w : Pattern 0) : Cylinder w = Set.univ := by
  37  ext s; constructor
  38  · intro _; exact Set.mem_univ _
  39  · intro _; exact (mem_Cylinder_zero w s)
  40
  41/-- Periodic extension of an 8‑bit window. -/
  42def extendPeriodic8 (w : Pattern 8) : Stream := fun t =>
  43  let h8 : 0 < 8 := by decide
  44  let i : Fin 8 := ⟨t % 8, Nat.mod_lt _ h8⟩
  45  w i
  46
  47@[simp] lemma extendPeriodic8_zero (w : Pattern 8) : extendPeriodic8 w 0 = w ⟨0, by decide⟩ := by
  48  simp [extendPeriodic8]
  49
  50@[simp] lemma extendPeriodic8_eq_mod (w : Pattern 8) (t : Nat) :
  51  extendPeriodic8 w t = w ⟨t % 8, Nat.mod_lt _ (by decide)⟩ := by
  52  rfl
  53
  54lemma extendPeriodic8_period (w : Pattern 8) (t : Nat) :
  55  extendPeriodic8 w (t + 8) = extendPeriodic8 w t := by
  56  dsimp [extendPeriodic8]
  57  have hmod : (t + 8) % 8 = t % 8 := by
  58    rw [Nat.add_mod]
  59    simp
  60  have h8 : 0 < 8 := by decide
  61  have hfin : (⟨(t + 8) % 8, Nat.mod_lt _ h8⟩ : Fin 8)
  62            = ⟨t % 8, Nat.mod_lt _ h8⟩ := by
  63    apply Fin.mk_eq_mk.mpr
  64    exact hmod
  65  rw [hfin]
  66
  67/-- Sum of the first `m` bits of a stream. -/
  68def sumFirst (m : Nat) (s : Stream) : Nat :=
  69  ∑ i : Fin m, (if s i.val then 1 else 0)
  70
  71/-- Base case: the sum of the first 0 bits is 0. -/
  72@[simp] lemma sumFirst_zero (s : Stream) : sumFirst 0 s = 0 := by
  73  simp [sumFirst]
  74
  75/-- If a stream agrees with a window on its first `n` bits, then the first‑`n` sum equals `Z`. -/
  76lemma sumFirst_eq_Z_on_cylinder {n : Nat} (w : Pattern n)
  77  {s : Stream} (hs : s ∈ Cylinder w) :
  78  sumFirst n s = Z_of_window w := by
  79  unfold sumFirst Z_of_window Cylinder at *
  80  have : (fun i : Fin n => (if s i.val then 1 else 0)) =
  81         (fun i : Fin n => (if w i then 1 else 0)) := by
  82    funext i; simp [hs i]
  83  simp [this]
  84
  85/-- For an 8‑bit window extended periodically, the first‑8 sum equals `Z`. -/
  86lemma sumFirst8_extendPeriodic_eq_Z (w : Pattern 8) :
  87  sumFirst 8 (extendPeriodic8 w) = Z_of_window w := by
  88  classical
  89  unfold sumFirst Z_of_window extendPeriodic8
  90  have hmod : ∀ i : Fin 8, (i.val % 8) = i.val := by
  91    intro i; exact Nat.mod_eq_of_lt i.isLt
  92  have h8 : 0 < 8 := by decide
  93  have hfun :
  94    (fun i : Fin 8 => (if w ⟨i.val % 8, Nat.mod_lt _ h8⟩ then 1 else 0))
  95    = (fun i : Fin 8 => (if w i then 1 else 0)) := by
  96      funext i; simp [hmod i]
  97  -- Now the two sums are definitionally equal by hfun.
  98  have := congrArg (fun f => ∑ i : Fin 8, f i) hfun
  99  simpa using this
 100
 101lemma extendPeriodic8_in_cylinder (w : Pattern 8) : (extendPeriodic8 w) ∈ (Cylinder w) := by
 102  intro i
 103  dsimp [extendPeriodic8, Cylinder]
 104  have hmod : (i.val % 8) = i.val := Nat.mod_eq_of_lt i.isLt
 105  simp [hmod]
 106
 107lemma sumFirst_nonneg (m : Nat) (s : Stream) : 0 ≤ sumFirst m s := by
 108  unfold sumFirst
 109  apply Finset.sum_nonneg
 110  intro i _
 111  split
 112  · norm_num
 113  · norm_num
 114
 115lemma sumFirst_eq_zero_of_all_false {m : Nat} {s : Stream}
 116  (h : ∀ i : Fin m, s i.val = false) :
 117  sumFirst m s = 0 := by
 118  unfold sumFirst
 119  have : (fun i : Fin m => (if s i.val then 1 else 0)) = (fun _ => 0) := by
 120    funext i; simp [h i]
 121  simp [this]
 122
 123end Streams
 124
 125end IndisputableMonolith
 126