39lemma sumFirst_eq_Z_on_cylinder {n : Nat} (w : Pattern n) 40 {s : Stream} (hs : s ∈ Cylinder w) : 41 sumFirst n s = Z_of_window w := by
proof body
Tactic-mode proof.
42 classical 43 unfold sumFirst Z_of_window Cylinder at * 44 have : (fun i : Fin n => (if s i.val then 1 else 0)) = 45 (fun i : Fin n => (if w i then 1 else 0)) := by 46 funext i; simpa [hs i] 47 simpa [this] 48 49/-- For an 8‑bit window extended periodically, the first‑8 sum equals `Z`. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.