fundamental_theorem_composite
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove existence or explicit construction of the recognition quotient.
- Does not extend the statement to infinite families of recognizers.
- Does not address topological or continuity properties of the quotient map.
- Does not instantiate the result with concrete physical constants or phi-tiers.
formal statement (Lean)
104theorem fundamental_theorem_composite {C E₁ E₂ : Type*}
105 [ConfigSpace C] [EventSpace E₁] [EventSpace E₂]
106 (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) (c₁ c₂ : C) :
107 recognitionQuotientMk (r₁ ⊗ r₂) c₁ = recognitionQuotientMk (r₁ ⊗ r₂) c₂ ↔
108 (r₁.R c₁ = r₁.R c₂ ∧ r₂.R c₁ = r₂.R c₂) := by
proof body
Term-mode proof.
109 rw [quotientMk_eq_iff]
110 exact composite_indistinguishable_iff r₁ r₂ c₁ c₂
111
112/-! ## Universal Property of the Recognition Quotient -/
113
114/-- **UNIVERSAL PROPERTY THEOREM**
115
116 The recognition quotient C_R has a universal property: it is the
117 "finest" quotient on which R factors through an injective map.
118
119 More precisely: For any quotient C → Q such that R factors through Q
120 (i.e., indistinguishable configs in C map to the same element of Q),
121 there exists a unique map C_R → Q making the diagram commute.
122
123 ```
124 C ----R----> E
125 | ↗
126 π R̄ (injective)
127 ↓ ↗
128 C_R ----→ Q
129 ```
130
131 This says: C_R is characterized by a universal property, not just
132 a construction. It is THE canonical quotient for recognition. -/