resolutionCells_partition
plain-language theorem explainer
Resolution cells partition the configuration space by establishing that each configuration c belongs to exactly one equivalence class under the recognizer-induced indistinguishability relation. Researchers modeling lossy recognition in geometry or physics would cite this to confirm unique cells for any given event. The proof is a direct term-mode construction that applies self-membership of the cell and equality to discharge uniqueness.
Claim. For any configuration $c$ in the space $C$, there exists a unique subset $cell$ of $C$ such that $c$ belongs to $cell$ and $cell$ coincides with the equivalence class of $c$ under the recognizer $r$.
background
The module develops Recognition Geometry axiom RG3: given a recognition map from configurations $C$ to events $E$, the indistinguishability relation is defined by $c_1$ equivalent to $c_2$ precisely when they produce the same event. Resolution cells are the equivalence classes of this relation, i.e., the sets of all configurations that map to one fixed event. The local setting treats these classes as the smallest distinguishable units of configuration space under a fixed recognizer.
proof idea
The term proof explicitly supplies the candidate cell as the resolution cell of $c$, verifies membership by the self-inclusion property, and discharges uniqueness by reducing any other qualifying cell to equality with the supplied one via the defining condition.
why it matters
The result completes the partition property for resolution cells inside the Indistinguishable module, directly supporting the downstream status declaration that records the full RG3 development. It anchors the framework's treatment of lossy recognition by guaranteeing that equivalence classes are canonically determined, consistent with the broader Recognition Science emphasis on unique resolution under the composition law and forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.