fundamental_theorem

formal source

  95    the recognizer assigns them the same event.
  96
  97    This is the cornerstone: observable space = C / {same events}. -/
  98theorem fundamental_theorem {C E : Type*} [ConfigSpace C] [EventSpace E]
  99    (r : Recognizer C E) (c₁ c₂ : C) :
 100    recognitionQuotientMk r c₁ = recognitionQuotientMk r c₂ ↔ r.R c₁ = r.R c₂ :=
 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