finite_resolution_pos
Finite resolution neighborhoods in recognition geometry contain at least one distinguishable event. Researchers modeling discrete spacetime at Planck scales would cite this to guarantee positive event counts inside local neighborhoods. The proof extracts the witnessing neighborhood and finiteness witness directly from the hypothesis then invokes the positivity lemma for finite event sets.
claimLet $L$ be a local configuration space over $C$ and $r$ a recognizer. If configuration $c$ satisfies finite local resolution under $L$ and $r$, then there exists a neighborhood $U$ in the neighborhood system of $c$ such that the image of $U$ under $r.R$ is finite and the event count of this finite image is strictly positive.
background
The Recognition Geometry module RG4 formalizes the axiom that recognition admits only finite local resolution: for every configuration $c$ and recognizer $r$ there exists a neighborhood $U$ around $c$ such that $r.R(U)$ is finite. HasFiniteLocalResolution $L$ $r$ $c$ is the predicate asserting exactly this existence of $U$ in $L.N(c)$ with the image finite. The module sits inside the broader Recognition Science setting where the 8-tick cycle supplies the atomicity that makes such finiteness fundamental rather than approximate.
proof idea
The proof is a one-line term wrapper. It obtains the neighborhood $U$ and finiteness witness $hfin$ from the hypothesis, then applies the lemma eventCountFinite_pos to the pair consisting of the recognizer image at $c$ together with the membership proof that $c$ lies in $U$.
why it matters in Recognition Science
This result secures the positivity half of the finite-resolution axiom RG4, ensuring that every local neighborhood contains at least one distinguishable event. It directly supports the physical reading that finite resolution arises from the 8-tick octave rather than from measurement limits. No downstream theorems are recorded yet, so the lemma remains a foundational closure for the discreteness claim in the Recognition Geometry layer.
scope and limits
- Does not supply an explicit upper bound on the event count.
- Does not extend the claim to neighborhoods without the finite-resolution hypothesis.
- Does not address global or infinite-resolution geometries.
formal statement (Lean)
143theorem finite_resolution_pos (c : C) (h : HasFiniteLocalResolution L r c) :
144 ∃ U ∈ L.N c, ∃ hfin : (r.R '' U).Finite, 0 < eventCountFinite (r.R '' U) hfin := by
proof body
Term-mode proof.
145 obtain ⟨U, hU, hfin⟩ := h
146 use U, hU, hfin
147 apply eventCountFinite_pos
148 exact ⟨r.R c, c, L.mem_of_mem_N c U hU, rfl⟩
149
150/-! ## Physical Interpretation -/
151
152/-- **Physical Interpretation**: In Recognition Science, finite resolution
153 corresponds to the 8-tick atomicity. The number of distinguishable
154 states in any local region is bounded by the number of ledger updates
155 that can occur in that region.
156
157 This is not an approximation or limitation of measurement—it is a
158 fundamental feature of reality as described by recognition geometry. -/