stability_forces_recognition

formal source

 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) ∧
 172    (∀ (S : JStableStructure),
 173      ∃ (R : RecognitionLikeStructure), R.carrier = S.carrier) :=
 174  ⟨recognition_necessary,
 175   fun _ M => ⟨recognition_from_extraction M, trivial⟩,
 176   recognition_is_cost_structure,
 177   cost_minima_are_recognition,
 178   stability_forces_recognition⟩