quotientMapRight_surjective
plain-language theorem explainer
The theorem shows that the natural projection from the composite recognizer quotient onto the second component quotient is surjective. Researchers formalizing how multiple measurements refine configuration space in Recognition Geometry cite it as one half of the Refinement Theorem. The term proof lifts an arbitrary class to a representative configuration via Quotient.exists_rep and maps it forward under the composite recognition quotient constructor.
Claim. Let $R_1$ and $R_2$ be recognizers on configuration space $C$. The natural projection map from the quotient induced by the composite recognizer $R_1 ⊗ R_2$ onto the quotient induced by $R_2$ is surjective.
background
In this module a Recognizer on $C$ is a map that partitions configurations into equivalence classes under indistinguishability, yielding a quotient space. The composite recognizer is the pointwise pair $(R_1(c), R_2(c))$, whose induced quotient is finer than either factor. quotientMapRight is the canonical projection that forgets the first component of the pair and passes to the quotient of $R_2$ alone. The module develops the theory of such composites and proves that the resulting quotient refines both input quotients, so that richer geometry emerges from simultaneous measurements.
proof idea
The proof is a direct term-mode construction. It takes an arbitrary class $q$ in the target quotient, extracts a representative configuration $c$ by the universal property of quotients, builds the preimage as the class of $c$ under the composite recognizer, and closes by reflexivity.
why it matters
This lemma supplies the right-hand surjectivity half of the Refinement Theorem, the central result of the module. The Refinement Theorem asserts that the composite quotient admits surjective maps onto each component quotient, formalizing the statement that combining recognizers yields a strictly finer view of configuration space. In the broader Recognition Science setting the result supports the emergence of additional structure from the Recognition Composition Law and is consistent with the eight-tick octave and the forcing of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.