recognition_from_extraction

formal source

  93  self_recognition : ∀ s, recognizes s s
  94  symmetric : ∀ s₁ s₂, recognizes s₁ s₂ → recognizes s₂ s₁
  95
  96def recognition_from_extraction {S : Type} (M : ObservableExtractionMechanism S) :
  97    RecognitionStructure S := {
  98  recognizes := fun s₁ s₂ => M.extract s₁ = M.extract s₂
  99  self_recognition := fun _ => rfl
 100  symmetric := fun _ _ h => h.symm
 101}
 102
 103/-- Recognition is unique extraction mechanism. -/
 104theorem recognition_unique {S : Type} (M : ObservableExtractionMechanism S) :
 105    ∃ R : RecognitionStructure S,
 106    (∀ s₁ s₂, M.extract s₁ = M.extract s₂ ↔ R.recognizes s₁ s₂) :=
 107  ⟨recognition_from_extraction M, fun _ _ => Iff.rfl⟩
 108
 109/-! ## Part 2: Cost Minima = Recognition -/
 110
 111structure Configuration where
 112  value : ℝ
 113  pos : 0 < value
 114
 115def config_to_recognition (c : Configuration) : LedgerForcing.RecognitionEvent :=
 116  { source := 0, target := 0, ratio := c.value, ratio_pos := c.pos }
 117
 118theorem cost_minima_are_recognition (c : Configuration) :
 119    ∃ (e : LedgerForcing.RecognitionEvent), e.ratio = c.value :=
 120  ⟨config_to_recognition c, rfl⟩
 121
 122theorem global_minimum_is_self_recognition :
 123    ∃ (e : LedgerForcing.RecognitionEvent), e.ratio = 1 ∧ recognition_cost e = 0 := by
 124  use { source := 0, target := 0, ratio := 1, ratio_pos := one_pos }
 125  simp only [recognition_cost, LedgerForcing.J]
 126  norm_num