separating_quotient_bijective
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.
claimIf 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 in Recognition Science
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.
scope and limits
- Does not prove existence of any separating recognizer for a given space.
- Does not compute the numerical value of recognition dimension.
- Does not treat non-separating or partially separating recognizers.
- Does not link the quotient construction to the phi-ladder or mass formulas.
formal statement (Lean)
51theorem separating_quotient_bijective (r : Recognizer C E) (h : IsSeparating r) :
52 Function.Bijective (recognitionQuotientMk r) := by
proof body
Term-mode proof.
53 constructor
54 · -- Injective
55 intro c₁ c₂ heq
56 have hindist : Indistinguishable r c₁ c₂ := (quotientMk_eq_iff r).mp heq
57 exact h hindist
58 · -- Surjective
59 intro q
60 obtain ⟨c, hc⟩ := Quotient.exists_rep q
61 use c
62 simp only [recognitionQuotientMk]
63 exact hc
64
65/-- If a recognizer separates, every resolution cell is a singleton. -/