fundamental_theorem_composite

formal source

 101  quotientMk_eq_iff r
 102
 103/-- **Extended Fundamental Theorem** for composite recognizers. -/
 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
 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. -/
 133theorem universal_property {C E : Type*} [ConfigSpace C] [EventSpace E]
 134    (r : Recognizer C E) :