localResolution_covers
plain-language theorem explainer
Local resolution cells induced by a recognizer on a set U of configurations recover U exactly under union. Workers in recognition geometry cite this result to establish that the partition into indistinguishability classes covers the domain. The proof applies set extensionality followed by direct membership chasing using the definition of LocalResolution and the fact that each configuration belongs to its own resolution cell.
Claim. Let $r$ be a recognizer from configurations $C$ to events $E$. For any subset $U$ of $C$, the union over all intersections $U$ with resolution cells of points in $U$ equals $U$.
background
In Recognition Geometry a recognizer induces an indistinguishability relation on configurations: two configurations are equivalent precisely when they produce the same event. The resolution cell of a configuration is its equivalence class under this relation, the smallest unit distinguishable by the recognizer. LocalResolution collects, for each point in $U$, the intersection of $U$ with that point's resolution cell, yielding the pieces of a partition of $U$.
proof idea
The proof proceeds by set extensionality on the union. One inclusion extracts the witness configuration from the intersecting cell. The converse direction builds the specific intersection $U$ with the resolution cell of the given point and applies the self-membership lemma for resolution cells.
why it matters
This result confirms that the local-resolution construction exhausts any chosen set of configurations, directly supporting the partition property required by the indistinguishability axiom in the module. It closes the cover direction for the equivalence classes defined by the recognizer and supplies the set-theoretic foundation needed before distinguishability statements can be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.