sumFirst8_extendPeriodic_eq_Z

formal source

  47  simpa [this]
  48
  49/-- For an 8‑bit window extended periodically, the first‑8 sum equals `Z`. -/
  50lemma sumFirst8_extendPeriodic_eq_Z (w : Pattern 8) :
  51  sumFirst 8 (extendPeriodic8 w) = Z_of_window w := by
  52  classical
  53  unfold sumFirst Z_of_window extendPeriodic8
  54  have hmod : ∀ i : Fin 8, (i.val % 8) = i.val := by
  55    intro i; exact Nat.mod_eq_of_lt i.isLt
  56  have hfun :
  57    (fun i : Fin 8 => (if w ⟨i.val % 8, Nat.mod_lt _ (by decide)⟩ then 1 else 0))
  58    = (fun i : Fin 8 => (if w i then 1 else 0)) := by
  59      funext i; simp [hmod i]
  60  have := congrArg (fun f => ∑ i : Fin 8, f i) hfun
  61  simpa using this
  62
  63end PatternLayer
  64
  65namespace MeasurementLayer
  66
  67open scoped BigOperators
  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}