injectivity_of_observable_map
plain-language theorem explainer
The induced map from quotiented recognizer configurations to events is injective. Authors of recognition-based observation models would cite it to guarantee distinct configuration classes produce distinct observables. The proof is a direct term application of the base injectivity lemma for quotient event maps.
Claim. Let $r$ be a recognizer from configuration space $C$ to event space $E$. The induced quotient map from the equivalence classes of configurations to $E$ is injective.
background
A Recognizer pairs a configuration space with an event space while satisfying the Recognition Composition Law, the multiplicative form of the d'Alembert equation $F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)$. The quotientEventMap extracts the observable map by collapsing equivalent configurations under the recognizer relation. This declaration lives in the DraftV1 module, whose purpose is to mirror theorem statements from Draft_v1.tex and re-export proved results under paper-oriented names when the underlying geometry (Alexander duality, quotient constructions) is already certified.
proof idea
The proof is a one-line term wrapper that applies quotientEventMap_injective to the supplied recognizer r.
why it matters
The result supplies the injectivity half of the refinement theorem for composite recognizers in Draft_v1.tex. It closes a necessary step before the composition of recognizers can be shown to preserve distinctions, consistent with the J-uniqueness and phi-forcing steps of the unified chain. No downstream uses are recorded yet, leaving open whether the same injectivity lifts to the full synchronization and selection principles listed as siblings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.