resolutionCell_eq_fiber
plain-language theorem explainer
The theorem states that for any recognizer the resolution cell of a configuration equals the fiber of the recognizer map over the event it produces. Workers on recognition geometry or lossy mappings cite it when they need to identify equivalence classes with preimages. The proof is a one-line wrapper that applies set extensionality and then simplifies using the definitions of indistinguishability and fibers.
Claim. Let $r : C → E$ be a recognizer. For any configuration $c ∈ C$, the resolution cell of $c$, defined as the set of all $c' ∈ C$ such that $r(c') = r(c)$, equals the fiber $r^{-1}(r(c))$.
background
Recognition geometry module RG3 introduces the indistinguishability relation on configurations induced by a recognizer map $r : C → E$. Two configurations are indistinguishable precisely when they map to the same event. The resolution cell of a configuration is its equivalence class under this relation, i.e., the set of all configurations that produce the identical event. The upstream definition of indistinguishability supplies the predicate $r(c_1) = r(c_2)$ that directly populates the resolution cell set.
proof idea
The proof applies set extensionality to equate the two sides, then simplifies the membership predicate using the definitions of ResolutionCell, Indistinguishable, and the fiber operation on the recognizer.
why it matters
This equality identifies resolution cells with fibers, confirming that the equivalence classes of RG3 are exactly the level sets of the recognition map. It is invoked inside the module status declaration that records completion of the indistinguishability axioms. The result closes the basic identification step in the recognition geometry layer before downstream results on distinguishable configurations are stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.