blockSumAligned8_periodic

formal source

 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
 130    simpa using
 131      (Finset.card_univ : Fintype.card (Fin k) = k) ▸
 132      (by simpa using (Finset.sum_const_natural (s:=Finset.univ) (a:=Z_of_window w)))
 133  have hmap := congrArg (fun f => ∑ j : Fin k, f j) (funext hconst)
 134  simpa using hmap.trans hsum
 135
 136/-- Averaged (per‑window) observation equals `Z` on periodic extensions. -/
 137def observeAvg8 (k : Nat) (s : Stream) : Nat :=
 138  blockSumAligned8 k s / k
 139
 140/-- DNARP Eq. (blockSum=Z at T=8k): on the periodic extension of an 8‑bit window,
 141    the per‑window averaged observation equals the window integer `Z`. -/
 142lemma observeAvg8_periodic_eq_Z {k : Nat} (hk : k ≠ 0) (w : Pattern 8) :
 143  observeAvg8 k (extendPeriodic8 w) = Z_of_window w := by
 144  classical
 145  unfold observeAvg8
 146  have hsum := blockSumAligned8_periodic w k
 147  have : (k * Z_of_window w) / k = Z_of_window w := by
 148    exact Nat.mul_div_cancel_left (Z_of_window w) (Nat.pos_of_ne_zero hk)
 149  simpa [hsum, this]
 150
 151end MeasurementLayer
 152
 153/-! ## Examples (witnesses) -/