pith. machine review for the scientific record. sign in
lemma proved tactic proof

firstBlockSum_eq_Z_on_cylinder

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  80lemma firstBlockSum_eq_Z_on_cylinder (w : Pattern 8) {s : Stream}
  81  (hs : s ∈ PatternLayer.Cylinder w) :
  82  subBlockSum8 s 0 = Z_of_window w := by

proof body

Tactic-mode proof.

  83  classical
  84  have hsum : subBlockSum8 s 0 = PatternLayer.sumFirst 8 s := by
  85    unfold subBlockSum8 PatternLayer.sumFirst
  86    simp [Nat.zero_mul, zero_add]
  87  simpa [hsum] using
  88    (PatternLayer.sumFirst_eq_Z_on_cylinder (n:=8) w (s:=s) hs)
  89
  90/-- Alias (T=8k, first block): if `s` is in the cylinder of `w`, then the
  91    aligned block sum over the first 8‑tick block equals `Z(w)`. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (38)

Lean names referenced from this declaration's body.

… and 8 more