IndisputableMonolith.RecogGeom.FiniteResolution
The FiniteResolution module defines finite local resolution for recognizers in Recognition Geometry. It states that a recognizer has finite local resolution at a point when some neighborhood observes only finitely many distinct events. Researchers developing local coordinate systems or foundational theorems cite these definitions. The module supplies predicates and basic monotonicity properties that rest on the recognition quotient construction.
claimA recognizer $R$ has finite local resolution at point $c$ when there exists a neighborhood $U$ of $c$ such that the set of distinct events observed in $U$ is finite. Related predicates include HasFiniteResolution and eventCount being finite.
background
Recognition Geometry begins with the quotient $C_R = C / {~}$ constructed in the Quotient module, where ${~}$ is the indistinguishability relation that collapses configurations the recognizer cannot separate. This module adds the finite-resolution layer on top of that quotient. It introduces HasFiniteLocalResolution, HasFiniteResolution, eventCount, and IsLocallyDiscrete to enforce that locally only finitely many events appear. These notions supply the local discreteness needed before charts or integration can proceed.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the finite-resolution predicates that Charts, Foundations, Integration, and RSBridge import. Charts uses them to build local coordinates; Foundations invokes them among the three pillars; Integration assembles the full framework; RSBridge connects the geometry to the 8-tick cycle and ledger states of Recognition Science. It therefore closes the local-finiteness step required for the geometric side of the T0-T8 chain.
scope and limits
- Does not prove global finiteness of events over the whole space.
- Does not establish existence of finite resolution for arbitrary recognizers.
- Does not incorporate phi-ladder mass formulas or alpha-band constraints.
- Does not treat continuous event distributions beyond the finite-count predicate.
- Does not supply counterexamples showing when finite resolution fails.
used by (4)
depends on (1)
declarations in this module (16)
-
def
HasFiniteLocalResolution -
def
HasFiniteResolution -
theorem
finite_resolution_event_in_finite -
theorem
finite_resolution_mono -
theorem
finite_resolution_cell_finite_events -
def
IsLocallyDiscrete -
theorem
locally_discrete_finite_classes -
theorem
no_injection_on_infinite_finite -
theorem
finite_resolution_not_injective -
def
eventCount -
theorem
eventCount_pos -
def
eventCountFinite -
theorem
eventCountFinite_pos -
theorem
finite_resolution_pos -
theorem
physical_interpretation_finite_resolution -
def
finite_resolution_status