subBlockSum8_periodic_eq_Z

formal source

  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]
 111                  using (Nat.add_mod (j*8) i.val 8)
 112      _   = (0 + i.val) % 8 := by simpa [h0, Nat.mod_eq_of_lt hi]
 113      _   = i.val % 8 := by simp
 114      _   = i.val := by simpa [Nat.mod_eq_of_lt hi]
 115  have hfun :
 116    (fun i : Fin 8 => (if w ⟨(j*8 + i.val) % 8, Nat.mod_lt _ (by decide)⟩ then 1 else 0))
 117    = (fun i : Fin 8 => (if w i then 1 else 0)) := by
 118      funext i; simp [hmod i]
 119  have := congrArg (fun f => ∑ i : Fin 8, f i) hfun
 120  simpa using this
 121
 122/-- For `s = extendPeriodic8 w`, summing `k` aligned 8‑blocks yields `k * Z(w)`. -/
 123lemma blockSumAligned8_periodic (w : Pattern 8) (k : Nat) :
 124  blockSumAligned8 k (extendPeriodic8 w) = k * Z_of_window w := by
 125  classical
 126  unfold blockSumAligned8
 127  have hconst : ∀ j : Fin k, subBlockSum8 (extendPeriodic8 w) j.val = Z_of_window w := by
 128    intro j; simpa using subBlockSum8_periodic_eq_Z w j.val
 129  have hsum : (∑ _j : Fin k, Z_of_window w) = k * Z_of_window w := by