pith. sign in
module module high

IndisputableMonolith.RecogGeom.FiniteResolution

show as:
view Lean formalization →

This module defines finite local resolution for recognizers on the recognition quotient, requiring a neighborhood with only finitely many distinct events. It would be cited by authors of recognition charts and foundational theorems in Recognition Geometry. The module supplies predicates, monotonicity lemmas, and event-count functions as scaffolding for downstream local coordinate and integration work.

claimA recognizer has finite local resolution at $c \in C_R$ when there exists a neighborhood $U$ of $c$ such that the set of observed events in $U$ is finite. The module also supplies the global predicate HasFiniteResolution, the eventCount function, and lemmas establishing monotonicity and local discreteness.

background

The module sits atop the recognition quotient $C_R = C/\sim$ constructed in the Quotient module, where $\sim$ is the indistinguishability relation that collapses configurations the recognizer cannot separate. It introduces the predicates HasFiniteLocalResolution and HasFiniteResolution together with the auxiliary functions eventCount and IsLocallyDiscrete. These notions formalize the requirement that only finitely many distinct events appear inside any sufficiently small neighborhood.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The finite-resolution predicates feed directly into the Charts module for local coordinate systems, the Foundations module for its three fundamental theorems, the Integration module for the complete framework summary, and the RSBridge module that links Recognition Geometry to the eight-tick cycle and ledger states of Recognition Science. Without these definitions the local-discreteness assumptions required by the fundamental theorems remain unstated.

scope and limits

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (16)