subBlockSum8

formal source

  68open Finset PatternLayer
  69
  70/-- Sum of one 8‑tick sub‑block starting at index `j*8`. -/
  71def subBlockSum8 (s : Stream) (j : Nat) : Nat :=
  72  ∑ i : Fin 8, (if s (j * 8 + i.val) then 1 else 0)
  73
  74/-- Aligned block sum over `k` copies of the 8‑tick window (so instrument length `T=8k`). -/
  75def blockSumAligned8 (k : Nat) (s : Stream) : Nat :=
  76  ∑ j : Fin k, subBlockSum8 s j.val
  77
  78/-- On any stream lying in the cylinder of an 8‑bit window, the aligned
  79    first block sum (j=0; T=8k alignment) equals the window integer `Z`. -/
  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
  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)`. -/
  92lemma blockSum_equals_Z_on_cylinder_first (w : Pattern 8) {s : Stream}
  93  (hs : s ∈ PatternLayer.Cylinder w) :
  94  blockSumAligned8 1 s = Z_of_window w := by
  95  classical
  96  simp [blockSumAligned8, firstBlockSum_eq_Z_on_cylinder w (s:=s) hs]
  97
  98/-- On periodic extensions of a window, each 8‑sub‑block sums to `Z`. -/
  99lemma subBlockSum8_periodic_eq_Z (w : Pattern 8) (j : Nat) :
 100  subBlockSum8 (extendPeriodic8 w) j = Z_of_window w := by
 101  classical