fundamental_theorem_composite
plain-language theorem explainer
The extended fundamental theorem for composite recognizers states that two configurations are identified by the recognition quotient of their tensor product if and only if each recognizer separately maps them to identical events. Researchers constructing multi-observer models or refining quotients in recognition geometry would cite this to justify tensor-product constructions. The proof is a one-line wrapper that rewrites the quotient equality and invokes the composite indistinguishability lemma.
Claim. Let $C$ be a configuration space and $E_1, E_2$ event spaces. For recognizers $r_1 : C → E_1$ and $r_2 : C → E_2$ and configurations $c_1, c_2 ∈ C$, the quotient map induced by the composite recognizer $r_1 ⊗ r_2$ satisfies $π_{r_1 ⊗ r_2}(c_1) = π_{r_1 ⊗ r_2}(c_2)$ if and only if $r_1(c_1) = r_1(c_2)$ and $r_2(c_1) = r_2(c_2)$.
background
Recognition Geometry equips a configuration space with families of recognizers that induce observable quotients. A ConfigSpace is an abstract structure carrying an empty configuration, a commutative join, a consistency predicate, and an independence relation. Recognizers map configurations to events in an EventSpace; the recognition quotient then collapses configurations that produce identical event outputs under a given recognizer. The module proves three pillars: the quotient determines all observables, additional recognizers strictly refine distinctions, and finite event spaces force coarse-graining. This theorem extends the basic equivalence between quotient classes and recognizer agreement to the tensor-product case.
proof idea
The proof is a one-line wrapper. It rewrites the left-hand side via the lemma quotientMk_eq_iff, which converts quotient equality into the indistinguishability predicate for the composite recognizer. It then applies the lemma composite_indistinguishable_iff, which decomposes the composite indistinguishability condition into the conjunction of the two component conditions.
why it matters
This result extends the core fundamental theorem of the module to composite recognizers, directly supporting the second pillar that more recognizers increase distinguishing power. It precedes and enables the universal-property theorem that characterizes the recognition quotient as the canonical finest quotient through which any recognizer factors. In the larger Recognition Science framework it justifies tensor products for multi-observer models while remaining consistent with the forcing chain and phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.