recognition_quotient_summary
plain-language theorem explainer
The recognition quotient theorem states that the canonical projection from configurations to the indistinguishability quotient is surjective while the induced event map to observables is injective. Recognition geometry researchers cite this result to establish that the quotient encodes precisely the observable distinctions without loss or duplication. The proof is a direct constructor: surjectivity follows from the existence of quotient representatives and injectivity is inherited from the prior event-map lemma.
Claim. Let $C$ be the space of configurations and $E$ the space of events. Let $R: C → E$ be a recognizer. Define the equivalence $c_1 ∼ c_2$ iff $R(c_1) = R(c_2)$. Let $C_R = C / ∼$ be the quotient space with projection $π: C → C_R$. Then $π$ is surjective and the induced map $R̄: C_R → E$ satisfying $R = R̄ ∘ π$ is injective.
background
The module constructs the recognition quotient $C_R = C / ∼$ where the indistinguishability relation identifies configurations that produce identical events under the recognizer $R: C → E$. The projection $π$ is realized by recognitionQuotientMk, which applies Quotient.mk to the indistinguishableSetoid. The induced event map quotientEventMap is defined by Quotient.lift of $R$, ensuring the diagram commutes: $R = R̄ ∘ π$ (see upstream doc-comment: 'The event map factors through the quotient'). Upstream Status classifies declarations as spec, derived, hypothesis or scaffold. The prior lemma quotientEventMap_injective establishes that $R̄$ separates distinct equivalence classes.
proof idea
The term-mode proof opens with constructor to split the conjunction. The left conjunct (surjectivity of recognitionQuotientMk) is discharged by intro q followed by obtain ⟨c, rfl⟩ := Quotient.exists_rep q and exact ⟨c, rfl⟩. The right conjunct is discharged by exact quotientEventMap_injective r, invoking the upstream injectivity theorem directly.
why it matters
This theorem confirms that the recognition quotient captures exactly the observable structure, closing the basic construction in RecogGeom.Quotient. It supplies the surjectivity and injectivity properties required for any downstream lifting or neighborhood arguments that treat the quotient as the space of distinguishable events. In the Recognition Science setting it aligns with the forcing chain by ensuring that only observable distinctions survive the quotient, consistent with the J-cost and phi-ladder reductions that eliminate unobservable degrees of freedom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.