pillar2_composite_refines

formal source

  67  composite_info_monotone_left r₁ r₂ h
  68
  69/-- **Corollary**: The composite quotient refines both component quotients. -/
  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₂) :=
  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. -/
  82theorem pillar3_finite_resolution_obstruction {C E : Type*}
  83    [ConfigSpace C] [EventSpace E]
  84    (L : LocalConfigSpace C) (r : Recognizer C E)
  85    (c : C) (U : Set C) (hU : U ∈ L.N c)
  86    (hinf : Set.Infinite U) (hfin : (r.R '' U).Finite) :
  87    ¬Function.Injective (r.R ∘ Subtype.val : U → E) :=
  88  no_injection_on_infinite_finite L r c U hU hinf hfin
  89
  90/-! ## The Fundamental Theorem -/
  91
  92/-- **FUNDAMENTAL THEOREM OF RECOGNITION GEOMETRY**
  93
  94    Two configurations are in the same equivalence class if and only if
  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₂ :=