OffTargetCost

formal source

  33    of `Jcost_pos_of_ne_one`). -/
  34def TurbulentCost : Prop := ∀ r : ℝ, 0 < r → r ≠ 1 → 0 < Jcost r
  35def DiseaseCost : Prop := ∀ r : ℝ, 0 < r → r ≠ 1 → 0 < Jcost r
  36def OffTargetCost : Prop := ∀ r : ℝ, 0 < r → r ≠ 1 → 0 < Jcost r
  37def OffEquilibriumGameCost : Prop := ∀ r : ℝ, 0 < r → r ≠ 1 → 0 < Jcost r
  38def MarketArbitrageGap : Prop := ∀ r : ℝ, 0 < r → r ≠ 1 → 0 < Jcost r
  39def BiasedReasoningCost : Prop := ∀ r : ℝ, 0 < r → r ≠ 1 → 0 < Jcost r
  40def RecognitionDeficit : Prop := ∀ r : ℝ, 0 < r → r ≠ 1 → 0 < Jcost r
  41
  42theorem turbulent_cost : TurbulentCost := fun r hr hne => Jcost_pos_of_ne_one r hr hne
  43theorem disease_cost : DiseaseCost := fun r hr hne => Jcost_pos_of_ne_one r hr hne
  44theorem off_target_cost : OffTargetCost := fun r hr hne => Jcost_pos_of_ne_one r hr hne
  45theorem off_equilibrium_game_cost : OffEquilibriumGameCost :=
  46  fun r hr hne => Jcost_pos_of_ne_one r hr hne
  47theorem market_arbitrage_gap : MarketArbitrageGap :=
  48  fun r hr hne => Jcost_pos_of_ne_one r hr hne
  49theorem biased_reasoning_cost : BiasedReasoningCost :=
  50  fun r hr hne => Jcost_pos_of_ne_one r hr hne
  51theorem recognition_deficit : RecognitionDeficit :=
  52  fun r hr hne => Jcost_pos_of_ne_one r hr hne
  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⁻¹ :=