CompositeRecognizer
plain-language theorem explainer
The CompositeRecognizer definition constructs a product recognizer from two input recognizers r₁ and r₂ by sending each configuration to the pair of their individual recognition events. Researchers modeling simultaneous measurements in Recognition Geometry cite this as the RG6 construction. The definition directly equips the product event space with the paired map and inherits nontriviality from the first component via a short tactic block.
Claim. Given recognizers $r_1 : Recognizer(C, E_1)$ and $r_2 : Recognizer(C, E_2)$, the composite recognizer $r_1 ⊗ r_2 : Recognizer(C, E_1 × E_2)$ is defined by $(r_1 ⊗ r_2)(c) = (r_1(c), r_2(c))$.
background
In Recognition Geometry a Recognizer on configuration space C with event space E consists of a map R : C → E together with a nontriviality condition ensuring distinct events exist. The module develops composition as RG6, showing how multiple recognizers acting on the same C produce a finer indistinguishability relation. The key insight is that the composite distinguishes configurations that either component distinguishes, yielding a larger quotient space.
proof idea
The definition assigns the recognition map as the product of the component maps. Nontriviality is established by pulling distinct events from r₁ and verifying the pair inequality via Prod.mk.injEq.
why it matters
This definition supplies the basic composite object used by composition_status to establish information monotonicity and the refinement theorem. It realizes RG6 in the Recognition framework, enabling the emergence of richer geometry from independent measurements as described in the module documentation. It connects to the broader program of deriving geometry from recognition without presupposing spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.