def definition def or abbrev

`hygienicBool`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  59def hygienicBool (p : Protocol) : Bool :=

proof body

Definition body.

  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. -/

depends on (7)

Lean names referenced from this declaration's body.

status in IndisputableMonolith.Constants.RSNativeUnits decl_use
Time in IndisputableMonolith.Constants.RSNativeUnits decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
status in IndisputableMonolith.Measurement.RSNative.Alignment decl_use
Protocol in IndisputableMonolith.Measurement.RSNative.Core decl_use
A in IndisputableMonolith.Modal.Actualization decl_use