  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
 112    (m : MultiplicativeRecognizer 𝒞) :
 113    MultiplicativeL4Polynomial m := by
 114  obtain ⟨P, hpoly, hsymm, hroute⟩ := m.laws.route_independence
 115  refine ⟨P, hpoly, hsymm, ?_⟩
 116  intro x y hx hy
 117  exact hroute x y hx hy
 118
 119/-- **L4 is automatic in the abstract form for any multiplicative recognizer.**
 120

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.