blockSumAligned8_periodic

formal source

  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. -/
  69structure Map (State Obs : Type) where
  70  T : ℝ
  71  T_pos : 0 < T
  72  meas : (ℝ → State) → ℝ → Obs
  73
  74/-- Midpoint sampling average (lightweight helper). -/
  75@[simp] noncomputable def avg (T : ℝ) (_hT : 0 < T) (x : ℝ → ℝ) (t : ℝ) : ℝ :=
  76  let tmid := t + T / 2
  77  x tmid
  78
  79/-- CQ (coherence quotient) descriptor with bounds witnessed explicitly. -/
  80structure CQ where
  81  listensPerSec : ℝ
  82  opsPerSec : ℝ
  83  coherence8 : ℝ
  84  coherence8_bounds :
  85    0 ≤ coherence8 ∧ 0 ≤ coherence8 ∧ coherence8 ≤ 1 ∧ coherence8 ≤ 1
  86
  87/-- CQ score; zero when the operations-per-second denominator vanishes. -/