Pith. sign in
module module high

IndisputableMonolith.RecogGeom.FiniteResolution

show as:
view Lean formalization →

The FiniteResolution module defines finite local resolution for recognizers on the recognition quotient. It would be cited when analyzing local event counts and discreteness in Recognition Geometry. The module supplies the core predicates HasFiniteLocalResolution and HasFiniteResolution together with their basic monotonicity and finiteness properties.

claimA recognizer has finite local resolution at point $c$ when there exists a neighborhood $U$ of $c$ such that only finitely many distinct events are observed inside $U$.

background

The module sits inside Recognition Geometry and imports the recognition quotient $C_R = C/\sim$ constructed in the Quotient module, where $\sim$ collapses indistinguishable configurations. It introduces the predicates HasFiniteLocalResolution and HasFiniteResolution, the function eventCount, and lemmas such as finite_resolution_mono and locally_discrete_finite_classes that relate local finiteness to the quotient structure.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module is imported by Charts, Foundations, Integration, and RSBridge. It supplies the finite-resolution notions required for the fundamental theorems of Recognition Geometry and for the bridge that instantiates the framework with the 8-tick cycle and ledger states of Recognition Science.

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)