refinement_theorem
plain-language theorem explainer
The refinement theorem states that for recognizers r1 and r2 on configuration space C the induced maps from the composite quotient to each component quotient are surjective. Modelers of multi-detector systems in recognition geometry cite it to justify finer partitions. The proof is a one-line wrapper pairing the left and right surjectivity lemmas.
Claim. Let $r_1 : C → E_1$ and $r_2 : C → E_2$ be recognizers. The natural projection from the quotient of the composite recognizer $r_{12}$ onto the quotient of $r_1$ is surjective, and likewise onto the quotient of $r_2$.
background
In Recognition Geometry module RG6 a composite recognizer is the product map $R_{12}(c) = (R_1(c), R_2(c))$. This yields the indistinguishability relation $c_1 ∼_{12} c_2$ iff both component relations hold, producing a finer partition of configuration space. The module states that the composite sees at least as much structure as either factor. Upstream the Composition axiom enforces the d'Alembert equation $F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)$ for cost functions on positive reals.
proof idea
The proof is a one-line wrapper that applies quotientMapLeft_surjective and quotientMapRight_surjective.
why it matters
This is the fundamental theorem of recognition composition; it directly supplies the paper theorem refinement in DraftV1 and the corollary pillar2_composite_refines in Foundations. The module doc calls it the result that the composite quotient refines both components, showing how richer geometry emerges from simpler measurements. It closes the basic composition step before associativity and commutativity results in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.