`recognizer_status`

definition

show as: view math explainer →

module: IndisputableMonolith.RecogGeom.Recognizer
domain: RecogGeom
line: 123 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.RecogGeom.Recognizer on GitHub at line 123.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 120
 121/-! ## Module Status -/
 122
 123def recognizer_status : String :=
 124  "✓ Recognizer structure defined (RG2)\n" ++
 125  "✓ LocalRecognizer combining locality and recognition\n" ++
 126  "✓ Nontriviality enforced by definition\n" ++
 127  "✓ Local image and fiber definitions\n" ++
 128  "✓ Fiber partition theorem\n" ++
 129  "✓ Event realization and witness\n" ++
 130  "\n" ++
 131  "RECOGNITION MAPS (RG2) COMPLETE"
 132
 133#eval recognizer_status
 134
 135end RecogGeom
 136end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.