rcl_direct_theorem

formal source

  97composition with the identity force `a = 0`, `b = 2`, and `c = 2`.
  98This is the self-contained algebraic proof used for the counted-once
  99subcase, independent of the d'Alembert inevitability theorem. -/
 100theorem rcl_direct_theorem
 101    (C : ComparisonOperator)
 102    (hOp : OperativePositiveRatioComparison C)
 103    (P : ℝ → ℝ → ℝ)
 104    (a b c d : ℝ)
 105    (hP : ∀ u v, P u v = a + b * u + c * v + d * u * v)
 106    (hSym : ∀ u v, P u v = P v u)
 107    (hCons : HasMultiplicativeConsistency (derivedCost C) P) :
 108    ∃ c0 : ℝ, ∀ u v, P u v = 2 * u + 2 * v + c0 * u * v := by
 109  have hF1 : derivedCost C 1 = 0 := by
 110    simpa [derivedCost] using hOp.identity 1 zero_lt_one
 111  rcases hOp.non_trivial with ⟨x0, hx0_pos, hx0_ne⟩
 112  let t := derivedCost C x0
 113  have ht_ne : t ≠ 0 := hx0_ne
 114
 115  have hCons11 := hCons 1 1 zero_lt_one zero_lt_one
 116  have hC11 : C 1 1 = 0 := hOp.identity 1 zero_lt_one
 117  have ha_zero : a = 0 := by
 118    have hp00 : P 0 0 = a := by
 119      simpa using hP 0 0
 120    have hzero : P 0 0 = 0 := by
 121      have htmp : 0 = P 0 0 := by
 122        simpa [derivedCost, hC11] using hCons11
 123      exact htmp.symm
 124    exact hp00 ▸ hzero
 125
 126  have hCons_x1 := hCons x0 1 hx0_pos zero_lt_one
 127  have hb_two : b = 2 := by
 128    have hmain : t + t = a + b * t := by
 129      simpa [derivedCost, t, hC11, hP] using hCons_x1
 130    have hprod : (2 - b) * t = 0 := by