LocalResolution
plain-language theorem explainer
The definition constructs, for any recognizer r and any subset U of configurations, the collection of all sets obtained by intersecting U with the resolution cell of each point inside U. Workers on recognition geometry cite it when establishing partitions or covering properties induced by lossy maps from configurations to events. The definition is realized by a direct set comprehension that references the prior ResolutionCell construction.
Claim. Let $r: C → E$ be a recognizer. For any subset $U ⊆ C$, the local resolution is the collection of all subsets $S ⊆ C$ such that $S = U ∩ [c]_r$ for some $c ∈ U$, where $[c]_r$ denotes the equivalence class of configurations that produce the same event as $c$ under $r$.
background
In the Recognition Geometry module, a recognizer is a map from configurations C to events E. Indistinguishability is the equivalence relation c₁ ~ c₂ iff r(c₁) = r(c₂); the resolution cell of c is therefore the full equivalence class {c' | r(c') = r(c)}. LocalResolution assembles the pieces U ∩ ResolutionCell r c for each c inside U, yielding the induced partition of U into units that remain distinguishable under this particular recognizer.
proof idea
The definition is a one-line set comprehension that directly invokes the earlier ResolutionCell construction: it collects every S that equals U intersected with the cell of some c ∈ U. No additional lemmas or tactics are required beyond the set-builder notation and the definition of membership in ResolutionCell.
why it matters
LocalResolution supplies the concrete partition used by the covering theorem localResolution_covers, which proves that the union of these pieces recovers U, and is referenced in the module status summary indistinguishable_status. It implements the partition aspect of axiom RG3, supplying the geometric units needed for later arguments about distinguishability in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.