structure
definition
Map
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Measurement on GitHub at line 69.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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