stable_to_recognition

formal source

 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),
 166      ∃ R : RecognitionStructure S, True) ∧
 167    (∀ (e : LedgerForcing.RecognitionEvent),
 168      (e.ratio = 1 ↔ recognition_cost e = 0) ∧
 169      (e.ratio ≠ 1 → recognition_cost e > 0)) ∧
 170    (∀ (c : Configuration),
 171      ∃ (e : LedgerForcing.RecognitionEvent), e.ratio = c.value) ∧