firstBlockSum_eq_Z_on_cylinder

formal source

  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
 102  unfold subBlockSum8 Z_of_window extendPeriodic8
 103  have hmod : ∀ i : Fin 8, ((j * 8 + i.val) % 8) = i.val := by
 104    intro i
 105    have hi : i.val < 8 := i.isLt
 106    have h0 : (j * 8) % 8 = 0 := by simpa using Nat.mul_mod j 8 8
 107    calc
 108      (j * 8 + i.val) % 8
 109          = ((j * 8) % 8 + i.val % 8) % 8 := by
 110                simpa [Nat.add_comm, Nat.add_left_comm, Nat.add_assoc, Nat.mul_comm]