IndisputableMonolith.Measurement

   1import Mathlib
   2import IndisputableMonolith.Streams
   3import IndisputableMonolith.Streams.Blocks
   4
   5/-!
   6Re-export of the eight-tick stream invariants used throughout the measurement layer,
   7plus a lightweight continuous-time measurement scaffold (CQ score).
   8-/
   9namespace IndisputableMonolith
  10namespace Measurement
  11
  12open PatternLayer
  13open MeasurementLayer
  14open Classical
  15
  16/-- Boolean streams as used by the measurement layer. -/
  17abbrev Stream := PatternLayer.Stream
  18
  19/-- Finite windows of length `n`. -/
  20abbrev Pattern (n : Nat) := PatternLayer.Pattern n
  21
  22/-- Integer functional counting ones in a window. -/
  23abbrev Z_of_window {n : Nat} (w : Pattern n) : Nat := PatternLayer.Z_of_window w
  24
  25/-- Cylinder set of streams matching a window. -/
  26abbrev Cylinder {n : Nat} (w : Pattern n) : Set Stream := PatternLayer.Cylinder w
  27
  28/-- Periodic extension of an 8-bit window. -/
  29abbrev extendPeriodic8 := PatternLayer.extendPeriodic8
  30
  31/-- Sum of the first `m` bits of a stream. -/
  32abbrev sumFirst (m : Nat) (s : Stream) : Nat := PatternLayer.sumFirst m s
  33
  34/-- Sum of one 8-tick sub-block starting at index `j * 8`. -/
  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. -/
  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. -/
  88@[simp] noncomputable def score (c : CQ) : ℝ :=
  89  if c.opsPerSec = 0 then 0 else (c.listensPerSec / c.opsPerSec) * c.coherence8
  90
  91end Measurement
  92end IndisputableMonolith
  93