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

core_status

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)

  86def core_status : String :=

proof body

Definition body.

  87  "✓ ConfigSpace defined (RG0)\n" ++
  88  "✓ EventSpace defined\n" ++
  89  "✓ Nonemptiness axiom established\n" ++
  90  "✓ Nontriviality axiom established\n" ++
  91  "✓ RecognitionTriple bundle defined\n" ++
  92  "\n" ++
  93  "CORE FOUNDATION COMPLETE"
  94
  95#eval core_status
  96
  97end RecogGeom
  98end IndisputableMonolith

depends on (7)

Lean names referenced from this declaration's body.