all_seven_are_one

formal source

  53
  54/-! ## Universality: all seven are definitionally the same proposition. -/
  55
  56theorem all_seven_are_one :
  57    TurbulentCost = DiseaseCost ∧
  58    DiseaseCost = OffTargetCost ∧
  59    OffTargetCost = OffEquilibriumGameCost ∧
  60    OffEquilibriumGameCost = MarketArbitrageGap ∧
  61    MarketArbitrageGap = BiasedReasoningCost ∧
  62    BiasedReasoningCost = RecognitionDeficit :=
  63  ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩
  64
  65/-- J-cost is symmetric around r = 1: J(r) = J(r⁻¹). -/
  66theorem symmetry_at_equilibrium (r : ℝ) (hr : 0 < r) : Jcost r = Jcost r⁻¹ :=
  67  Jcost_symm hr
  68
  69/-- The minimum of J on (0, ∞) is at r = 1, value 0. -/
  70theorem minimum_at_one : ∀ r : ℝ, 0 < r → Jcost 1 ≤ Jcost r := by
  71  intro r hr
  72  rw [Jcost_unit0]
  73  rcases eq_or_ne r 1 with heq | hne
  74  · rw [heq, Jcost_unit0]
  75  · exact le_of_lt (Jcost_pos_of_ne_one r hr hne)
  76
  77structure JPositivityUniversalityCert where
  78  turbulent : TurbulentCost
  79  disease : DiseaseCost
  80  off_target : OffTargetCost
  81  off_game : OffEquilibriumGameCost
  82  arbitrage : MarketArbitrageGap
  83  biased : BiasedReasoningCost
  84  deficit : RecognitionDeficit
  85  all_same : TurbulentCost = DiseaseCost ∧
  86             DiseaseCost = OffTargetCost ∧