config_to_recognition

formal source

 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
 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