theorem
proved
physical_interpretation_finite_resolution
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RecogGeom.FiniteResolution on GitHub at line 159.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
156
157 This is not an approximation or limitation of measurement—it is a
158 fundamental feature of reality as described by recognition geometry. -/
159theorem physical_interpretation_finite_resolution
160 (h : IsLocallyDiscrete L r) :
161 ∀ c, ∃ U ∈ L.N c, (r.R '' U).Finite := by
162 intro c
163 exact h c
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