blockSumAligned8

formal source

  35abbrev subBlockSum8 (s : Stream) (j : Nat) : Nat := MeasurementLayer.subBlockSum8 s j
  36
  37/-- Aligned block sum over `k` copies of the 8-tick window. -/
  38abbrev blockSumAligned8 (k : Nat) (s : Stream) : Nat := MeasurementLayer.blockSumAligned8 k s
  39
  40/-- Averaged (per-window) observation over aligned blocks. -/
  41abbrev observeAvg8 (k : Nat) (s : Stream) : Nat := MeasurementLayer.observeAvg8 k s
  42
  43/-- On any stream lying in the cylinder of an 8-bit window, the first block sum equals `Z`. -/
  44lemma firstBlockSum_eq_Z_on_cylinder (w : Pattern 8) {s : Stream}
  45    (hs : s ∈ Cylinder w) :
  46    subBlockSum8 s 0 = Z_of_window w := by
  47  simpa [subBlockSum8, Cylinder, Z_of_window]
  48    using MeasurementLayer.firstBlockSum_eq_Z_on_cylinder (w:=w) (s:=s) hs
  49
  50/-- For periodic extensions of an 8-bit window, each sub-block sums to `Z`. -/
  51lemma subBlockSum8_periodic_eq_Z (w : Pattern 8) (j : Nat) :
  52    subBlockSum8 (extendPeriodic8 w) j = Z_of_window w := by
  53  simpa [subBlockSum8, extendPeriodic8, Z_of_window]
  54    using MeasurementLayer.subBlockSum8_periodic_eq_Z (w:=w) j
  55
  56/-- For `s = extendPeriodic8 w`, summing `k` aligned 8-blocks yields `k * Z(w)`. -/
  57lemma blockSumAligned8_periodic (w : Pattern 8) (k : Nat) :
  58    blockSumAligned8 k (extendPeriodic8 w) = k * Z_of_window w := by
  59  simpa [blockSumAligned8, extendPeriodic8, Z_of_window]
  60    using MeasurementLayer.blockSumAligned8_periodic (w:=w) k
  61
  62/-- DNARP Eq.: on periodic extensions of an 8-bit window, the averaged observation equals `Z`. -/
  63lemma observeAvg8_periodic_eq_Z {k : Nat} (hk : k ≠ 0) (w : Pattern 8) :
  64    observeAvg8 k (extendPeriodic8 w) = Z_of_window w := by
  65  simpa [observeAvg8, extendPeriodic8, Z_of_window]
  66    using MeasurementLayer.observeAvg8_periodic_eq_Z (k:=k) (hk:=hk) (w:=w)
  67
  68/-- Minimal measurement map scaffold. -/