global_minimum_is_self_recognition

formal source

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