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

CPMClosureCert

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)

  18structure CPMClosureCert where
  19  deriving Repr
  20
  21/-- Verification predicate for the CPM closure certificate.
  22
  23Delegates to the standalone `CPMMethodCert` verification predicate. -/
  24@[simp] def CPMClosureCert.verified (_c : CPMClosureCert) : Prop :=

proof body

Definition body.

  25  CPMMethodCert.verified {}
  26
  27/-- Top-level theorem: CPM closure certificate verifies. -/
  28@[simp] theorem CPMClosureCert.verified_any (c : CPMClosureCert) :
  29  CPMClosureCert.verified c := by
  30  dsimp [CPMClosureCert.verified]
  31  exact CPMMethodCert.verified_any {}
  32
  33end URCGenerators
  34end IndisputableMonolith

used by (2)

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

depends on (4)

Lean names referenced from this declaration's body.