`finite_resolution_status`

definition

show as: view math explainer →

module: IndisputableMonolith.RecogGeom.FiniteResolution
domain: RecogGeom
line: 167 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.RecogGeom.FiniteResolution on GitHub at line 167.

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

 164
 165/-! ## Module Status -/
 166
 167def finite_resolution_status : String :=
 168  "✓ HasFiniteLocalResolution defined (RG4)\n" ++
 169  "✓ HasFiniteResolution: global finite resolution\n" ++
 170  "✓ finite_resolution_event_in_finite\n" ++
 171  "✓ finite_resolution_mono: inheritance by smaller neighborhoods\n" ++
 172  "✓ no_injection_on_infinite_finite: key non-injection theorem\n" ++
 173  "✓ finite_resolution_not_injective: corollary\n" ++
 174  "✓ eventCount, minResolution: counting distinct events\n" ++
 175  "✓ physical_interpretation_finite_resolution\n" ++
 176  "\n" ++
 177  "FINITE RESOLUTION (RG4) COMPLETE"
 178
 179#eval finite_resolution_status
 180
 181end RecogGeom
 182end IndisputableMonolith

papers checked against this theorem

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