pillar2_composite_refines
For any configuration space C and recognizers r1, r2 into event spaces E1 and E2, the induced quotient maps from the composite recognizer to each separate quotient are surjective. Recognition geometers cite this corollary to confirm that merging recognizers strictly refines observable distinctions without discarding information from either original. The proof is a direct one-line wrapper invoking the refinement theorem on the pair r1 and r2.
claimLet $C$ be a configuration space with empty element, commutative join, consistency predicate, and independence relation. Let $E_1$ and $E_2$ be event spaces and let $r_1$, $r_2$ be recognizers from $C$ to $E_1$ and $E_2$. Then the left and right quotient maps induced by the composite recognizer are both surjective.
background
A configuration space consists of an empty configuration, a binary join operation forming a commutative monoid, a consistency predicate, and a symmetric independence relation with the empty configuration independent of all others. Recognizers map configurations to events in their respective spaces, inducing quotients that identify indistinguishable configurations. The module states the three pillars of Recognition Geometry: the quotient determines observables, more recognizers yield finer resolution, and finite resolution is fundamental. This theorem belongs to the second pillar.
proof idea
The proof is a one-line wrapper that applies the refinement theorem directly to the pair of recognizers r1 and r2, discharging both surjectivity conjuncts simultaneously.
why it matters in Recognition Science
This result fills the second pillar by establishing that the composite quotient refines each component, feeding directly into the foundations_status summary of the three pillars. It supports the universal property that the recognition quotient is the coequalizer of the indistinguishability relation and aligns with the framework's emphasis on how additional recognizers increase distinguishing power without introducing new axioms.
scope and limits
- Does not prove the quotient maps are injective.
- Does not treat finite-resolution neighborhoods or obstruction results.
- Does not construct explicit representatives for the quotient maps.
- Does not invoke J-cost, phi-ladder, or numerical constants from the forcing chain.
formal statement (Lean)
70theorem pillar2_composite_refines {C E₁ E₂ : Type*}
71 [ConfigSpace C] [EventSpace E₁] [EventSpace E₂]
72 (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
73 Function.Surjective (quotientMapLeft r₁ r₂) ∧
74 Function.Surjective (quotientMapRight r₁ r₂) :=
proof body
Term-mode proof.
75 refinement_theorem r₁ r₂
76
77/-! ## Pillar 3: Finite Resolution is Fundamental -/
78
79/-- **Pillar 3 (Finite Resolution Obstruction)**: If a neighborhood has
80 infinitely many configurations but only finitely many events,
81 no injection exists. -/