`Window`

definition

show as: view math explainer →

module: IndisputableMonolith.Measurement.RSNative.Core
domain: Measurement
line: 70 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Measurement.RSNative.Core on GitHub at line 70.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  67/-! ## Time windows (ticks) -/
  68
  69/-- A discrete measurement window, expressed in ticks. -/
  70structure Window where
  71  /-- Start tick. -/
  72  t0 : Nat
  73  /-- Window length in ticks (0 = instantaneous). -/
  74  len : Nat
  75  deriving DecidableEq
  76
  77namespace Window
  78
  79@[simp] def instant (t : Nat) : Window := ⟨t, 0⟩
  80
  81@[simp] def stop (w : Window) : Nat := w.t0 + w.len
  82
  83end Window
  84
  85/-! ## Uncertainty and measurement record -/
  86
  87/-- Uncertainty semantics for scalar (real-valued) measurements.
  88
  89v1 used only `sigma`. v2 adds:
  90- interval bounds
  91- a finite discrete distribution scaffold
  92
  93This is intentionally lightweight: it is a *reporting seam* for measurement,
  94not a full probability theory. -/
  95inductive Uncertainty where
  96  /-- Symmetric 1σ uncertainty (standard deviation), in the same units as the value. -/
  97  | sigma (σ : ℝ) (hσ : 0 ≤ σ)
  98  /-- Interval uncertainty: the true value lies in `[lo, hi]`. -/
  99  | interval (lo hi : ℝ) (hlohi : lo ≤ hi)
 100  /-- Finite discrete distribution scaffold: list of `(value, weight)` pairs.

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.