`locality_status`

definition

show as: view math explainer →

module: IndisputableMonolith.RecogGeom.Locality
domain: RecogGeom
line: 130 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.RecogGeom.Locality on GitHub at line 130.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 127
 128/-! ## Module Status -/
 129
 130def locality_status : String :=
 131  "✓ LocalConfigSpace defined (RG1)\n" ++
 132  "✓ Neighborhood axioms: mem_of_mem_N, intersection_closed, refinement\n" ++
 133  "✓ Basic lemmas: has_neighborhood, self_mem_neighborhood, common_refinement\n" ++
 134  "✓ Neighborhood filter construction\n" ++
 135  "✓ Discrete and trivial examples\n" ++
 136  "\n" ++
 137  "LOCALITY STRUCTURE (RG1) COMPLETE"
 138
 139#eval locality_status
 140
 141end RecogGeom
 142end IndisputableMonolith

papers checked against this theorem

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