def
definition
hygienic
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Measurement.RSNative.Core on GitHub at line 52.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
49Rules:
50- `name` must be non-empty
51- if `status` is `.hypothesis` or `.scaffold`, both `assumptions` and `falsifiers` must be non-empty -/
52def hygienic (p : Protocol) : Prop :=
53 p.name ≠ "" ∧
54 match p.status with
55 | .hypothesis | .scaffold => p.assumptions ≠ [] ∧ p.falsifiers ≠ []
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