cost_def

formal source

  78noncomputable def cost (m : MultiplicativeRecognizer 𝒞) : ℝ → ℝ :=
  79  derivedCost m.comparator
  80
  81@[simp] theorem cost_def (m : MultiplicativeRecognizer 𝒞) (r : ℝ) :
  82    m.cost r = m.comparator r 1 := rfl
  83
  84/-! ## L4 in d'Alembert (Multiplicative) Form -/
  85
  86/-- The **multiplicative form of (L4)**: there exists a combiner `P` such
  87that the cost of the product comparison plus the cost of the quotient
  88comparison equals `P` evaluated on the component costs. This is the
  89d'Alembert form of route-independence on positive ratios. -/
  90def MultiplicativeL4 (m : MultiplicativeRecognizer 𝒞) : Prop :=
  91  ∃ P : ℝ → ℝ → ℝ,
  92    ∀ x y : ℝ, 0 < x → 0 < y →
  93      m.cost (x * y) + m.cost (x / y) = P (m.cost x) (m.cost y)
  94
  95/-- A polynomial-degree-2 form of (L4): the combiner is a polynomial of
  96total degree at most two. This is the form the d'Alembert Inevitability
  97Theorem produces. -/
  98def MultiplicativeL4Polynomial (m : MultiplicativeRecognizer 𝒞) : Prop :=
  99  ∃ P : ℝ → ℝ → ℝ,
 100    (∃ a b c d e f : ℝ, ∀ u v, P u v = a + b*u + c*v + d*u*v + e*u^2 + f*v^2) ∧
 101    (∀ u v, P u v = P v u) ∧
 102    (∀ x y : ℝ, 0 < x → 0 < y →
 103      m.cost (x * y) + m.cost (x / y) = P (m.cost x) (m.cost y))
 104
 105/-! ## The Derivation Theorem -/
 106
 107/-- **L4 is automatic in the polynomial form for any multiplicative recognizer.**
 108
 109The route-independence field of `SatisfiesLawsOfLogic` already provides the
 110polynomial-degree-2 combiner satisfying the multiplicative L4. -/
 111theorem multiplicativeRecognizer_satisfies_L4_polynomial