RecognitionLikeStructure

formal source

 132  cost : carrier → ℝ
 133  cost_bounded : ∃ m : ℝ, ∀ x, m ≤ cost x
 134
 135structure RecognitionLikeStructure where
 136  carrier : Type
 137  rel : carrier → carrier → Prop
 138  refl : ∀ x, rel x x
 139  symm : ∀ x y, rel x y → rel y x
 140
 141def stable_to_recognition (S : JStableStructure) : RecognitionLikeStructure := {
 142  carrier := S.carrier
 143  rel := fun x y => S.cost x = S.cost y
 144  refl := fun _ => rfl
 145  symm := fun _ _ h => h.symm
 146}
 147
 148theorem stability_forces_recognition (S : JStableStructure) :
 149    ∃ (R : RecognitionLikeStructure), R.carrier = S.carrier :=
 150  ⟨stable_to_recognition S, rfl⟩
 151
 152/-! ## Part 4: Master Theorem -/
 153
 154theorem recognition_necessary (S : Type) (obs : Observable S)
 155    (h : ∃ s₁ s₂, obs.value s₁ ≠ obs.value s₂) :
 156    ∃ (R₁ R₂ : Type), Nonempty (Recognition.Recognize R₁ R₂) := by
 157  obtain ⟨s₁, s₂, _⟩ := h
 158  exact ⟨S, S, ⟨⟨s₁, s₂⟩⟩⟩
 159
 160/-- **MASTER THEOREM: Recognition Forcing Complete** -/
 161theorem recognition_forcing_complete :
 162    (∀ (S : Type) (obs : Observable S),
 163      (∃ s₁ s₂, obs.value s₁ ≠ obs.value s₂) →
 164      ∃ (R₁ R₂ : Type), Nonempty (Recognition.Recognize R₁ R₂)) ∧
 165    (∀ (S : Type) (M : ObservableExtractionMechanism S),