separating_quotient_bijective
plain-language theorem explainer
A separating recognizer induces a bijective recognition quotient map from the configuration space to its quotient. Recognition geometers cite this to confirm that separation produces a faithful representation of configurations. The proof establishes bijectivity by reducing injectivity to the separating hypothesis via the quotient-equivalence lemma and surjectivity to the existence of representatives.
Claim. If a recognizer $r$ is separating (i.e., injective on the configuration space $C$), then the recognition quotient map induced by $r$ is bijective.
background
Recognition Geometry defines dimension operationally as the smallest number of independent recognizers needed to distinguish every configuration. A Recognizer consists of a map $r.R$ from configurations $C$ to some evidence space $E$. The predicate IsSeparating $r$ holds precisely when $r.R$ is injective, which is equivalent to saying no two distinct configurations are indistinguishable under $r$. The map recognitionQuotientMk $r$ sends each configuration to its equivalence class under the indistinguishability relation generated by $r$.
proof idea
The term proof applies the constructor tactic for Function.Bijective. Injectivity is obtained by rewriting quotient equality with the upstream lemma quotientMk_eq_iff to recover indistinguishability and then invoking the hypothesis that $r$ is separating. Surjectivity follows directly from the existence of a representative for every quotient element, followed by the definition of recognitionQuotientMk.
why it matters
This result anchors the dimension theory in the module by guaranteeing that a separating recognizer yields an isomorphism between $C$ and its quotient. It therefore supports the downstream dimension_status definition, which equates recognition dimension with the count of independent recognizers required for separation, and feeds the complete_summary of the geometry modules. The theorem aligns with the framework claim that spacetime dimension equals four because exactly four independent recognizers separate events.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.