refinement_theorem
The refinement theorem states that the quotient space of a composite recognizer surjects onto the quotient of each component recognizer. Researchers in recognition geometry cite it to establish that joint observations partition configuration space at least as finely as either factor alone. The proof is a one-line term that pairs the surjectivity lemmas for the left and right quotient maps.
claimLet $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 the projection onto the quotient of $R_2$ is likewise surjective.
background
In the Recognition Geometry composition module, a recognizer maps configurations to events and induces an indistinguishability equivalence whose quotient is the space of distinguishable classes. The composite recognizer is the product map sending each configuration to the pair of events from the two components, yielding a finer equivalence relation whose quotient is larger. The module proves that this composite quotient refines both factors, so the joint view sees at least as much structure as either component.
proof idea
The proof is a one-line term that pairs the two surjectivity statements. It applies the lemma quotientMapLeft_surjective to obtain the left projection and the lemma quotientMapRight_surjective to obtain the right projection, then packages the pair as a conjunction.
why it matters in Recognition Science
This is the central result of the Recognition Geometry composition module. It is invoked directly by the paper theorem on refinement and by the pillar2_composite_refines corollary in Foundations. The result formalizes how richer geometry emerges from combined recognizers, consistent with the module insight that the indistinguishability relation becomes finer under composition.
scope and limits
- Does not prove the quotient maps are injective.
- Does not compute the increase in the number of equivalence classes.
- Does not extend to infinite or continuous families of recognizers.
- Does not connect to the phi-ladder, mass formulas, or eight-tick octave.
Lean usage
theorem paper_refinement {C E₁ E₂ : Type*} (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) : Function.Surjective (quotientMapLeft r₁ r₂) ∧ Function.Surjective (quotientMapRight r₁ r₂) := refinement_theorem r₁ r₂formal statement (Lean)
154theorem refinement_theorem (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
155 Function.Surjective (quotientMapLeft r₁ r₂) ∧
156 Function.Surjective (quotientMapRight r₁ r₂) :=
proof body
Term-mode proof.
157 ⟨quotientMapLeft_surjective r₁ r₂, quotientMapRight_surjective r₁ r₂⟩
158
159/-! ## Associativity and Commutativity -/
160
161/-- Composition is commutative up to isomorphism on events -/