recognition_unique

formal source

 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
 127
 128/-! ## Part 3: Stability = Recognition -/
 129
 130structure JStableStructure where
 131  carrier : Type
 132  cost : carrier → ℝ
 133  cost_bounded : ∃ m : ℝ, ∀ x, m ≤ cost x
 134