refinement
plain-language theorem explainer
The refinement theorem asserts that for recognizers r1 and r2 sharing configuration space C, the induced maps from the composite quotient to each component quotient are surjective. Researchers formalizing recognition composition in Recognition Science cite this when establishing that merged recognizers yield covering but finer partitions of configuration space. The proof is a one-line wrapper invoking the upstream refinement_theorem from the Composition module.
Claim. Let $r_1$ and $r_2$ be recognizers on a shared configuration space $C$. The natural quotient maps from the composite recognizer $r_1 ⊗ r_2$ onto the individual quotients of $r_1$ and of $r_2$ are both surjective.
background
A Recognizer pairs a configuration space C with an event space E to define observable distinctions via equivalence classes. The composite r1 ⊗ r2 merges two such recognizers on the same C, inducing a finer RecognitionQuotient. The quotientMapLeft and quotientMapRight are the canonical projections from the composite quotient to each factor quotient, constructed via Quotient.lift using the refinement relations composite_refines_left and composite_refines_right.
proof idea
The proof is a one-line wrapper that applies refinement_theorem from the Composition module, which decomposes the claim into the pair of surjectivity statements for quotientMapLeft and quotientMapRight.
why it matters
This is the fundamental theorem of recognition composition, re-exported here to mirror the corresponding statement in Draft_v1.tex. It is invoked by downstream results including refinement_calibrated, refinement_discharge_inherits, and regge_sum_refinement_invariant in SimplicialLedger.CubicSimplicialEquivalence, as well as absLogVorticity in Flight.Medium. The result supports the Recognition Composition Law by guaranteeing coverage of the original quotients and feeds into simplicial refinement invariance used for Regge sums and phi-ladder calibrations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.