pith. machine review for the scientific record. sign in
structure definition def or abbrev

Protocol

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  33structure Protocol where
  34  /-- Short protocol identifier (stable, machine-friendly). -/
  35  name : String
  36  /-- Human-readable summary. -/
  37  summary : String := ""

proof body

Definition body.

  38  /-- Claim hygiene for the extraction step. -/
  39  status : Status := .spec
  40  /-- Explicit assumptions (kept small and testable). -/
  41  assumptions : List String := []
  42  /-- Falsifiers: what would prove this protocol wrong. -/
  43  falsifiers : List String := []
  44
  45namespace Protocol
  46
  47/-- Protocol hygiene predicate (v1/v2).
  48
  49Rules:
  50- `name` must be non-empty
  51- if `status` is `.hypothesis` or `.scaffold`, both `assumptions` and `falsifiers` must be non-empty -/

used by (10)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (13)

Lean names referenced from this declaration's body.