quotientNeighborhoods
plain-language theorem explainer
quotientNeighborhoods equips each point of the recognition quotient with the collection of all sets containing the projected image of some local neighborhood around a representative configuration. Researchers constructing the topology on observable equivalence classes would cite this when lifting local structure to the quotient. The definition is realized directly as a set comprehension that applies the canonical projection to neighborhoods from the local configuration space.
Claim. Let $C_R$ be the recognition quotient $C/{~}$ under indistinguishability. Given a local configuration space $L$ on $C$, the neighborhood assignment sends each $q$ in $C_R$ to the family of all $V$ such that there exists a representative $c$ with $q = [c]$ and a neighborhood $U$ of $c$ in $L$ whose image under the projection lies inside $V$.
background
The Recognition Geometry module constructs the recognition quotient $C_R = C/{~}$ where $c_1 ~ c_2$ precisely when the recognizer returns identical events. RecognitionQuotient is defined as the quotient by the indistinguishable setoid, with recognitionQuotientMk supplying the canonical projection map. projectSet sends a subset of $C$ to its image in the quotient by collecting all classes that intersect the subset.
proof idea
This is a direct definition that, for each quotient point q, collects all supersets V of the projected local neighborhoods around any representative c of q. It applies projectSet to the neighborhoods N c supplied by the local configuration space and uses recognitionQuotientMk to test membership of representatives.
why it matters
This definition supplies the neighborhood structure required to equip the recognition quotient with a topology inside the Recognition Geometry module. It is referenced by the downstream summary quotient_status, which records that the projection is surjective and the induced event map is injective, thereby confirming that the quotient captures exactly the observable structure. The construction aligns with the indistinguishability relation that collapses indistinguishable configurations throughout the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.