sumFirst_zero

formal source

  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