`hygienicBool`

definition

show as: view math explainer →

module: IndisputableMonolith.Measurement.RSNative.Core
domain: Measurement
line: 59 · 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 59.

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

formal source

  56    | _ => True
  57
  58/-- Boolean check version of `Protocol.hygienic` (useful for audits). -/
  59def hygienicBool (p : Protocol) : Bool :=
  60  (!p.name.isEmpty) &&
  61    match p.status with
  62    | .hypothesis | .scaffold => (!p.assumptions.isEmpty) && (!p.falsifiers.isEmpty)
  63    | _ => true
  64
  65end Protocol
  66
  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:

papers checked against this theorem

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