finite_resolution_status
plain-language theorem explainer
This definition supplies a concatenated status string that reports completion of the finite local resolution formalization (RG4) in recognition geometry. A physicist modeling discrete spacetime or a mathematician auditing the Recognition Science chain would reference it to verify that local discreteness, monotonicity, and non-injectivity results are in place. The construction is a direct string concatenation of checkmarks for each sibling lemma, with no computation or tactics required.
Claim. The completion status of finite local resolution is the string ``✓ HasFiniteLocalResolution defined (RG4) ✓ HasFiniteResolution: global finite resolution ... FINITE RESOLUTION (RG4) COMPLETE''.
background
The module formalizes axiom RG4: for every configuration c and recognizer R there exists a neighborhood U around c such that the image R(U) is finite. This encodes the constraint that any recognition geometry has finite local resolution, meaning a recognizer distinguishes only finitely many configurations inside any bounded neighborhood. The key sibling definition IsLocallyDiscrete L r holds precisely when HasFiniteResolution L r, i.e., every neighborhood contains only finitely many distinguishable events.
proof idea
The definition is a direct string concatenation that lists the status of each completed item in the module: HasFiniteLocalResolution, HasFiniteResolution, finite_resolution_event_in_finite, finite_resolution_mono, finite_resolution_not_injective, eventCount, and the physical interpretation theorem. It terminates with the completion banner. No lemmas are applied; the body is literal text assembly.
why it matters
The declaration closes the RG4 section of the Recognition Geometry development, confirming that the 8-tick atomicity (T7) forces finite local resolution and thereby discrete geometries. It supplies the bridge from the Recognition Composition Law to the appearance of discrete spacetime at fundamental scales, consistent with the phi-ladder mass formula and the alpha band. No downstream theorems depend on it; it functions as a module-level summary rather than a lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.