MultiplicativeL4Polynomial

formal source

  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
 121The polynomial form trivially gives the existence form. -/
 122theorem multiplicativeRecognizer_satisfies_L4
 123    (m : MultiplicativeRecognizer 𝒞) :
 124    MultiplicativeL4 m := by
 125  obtain ⟨P, _, _, hroute⟩ := multiplicativeRecognizer_satisfies_L4_polynomial m
 126  exact ⟨P, hroute⟩
 127
 128/-- **The (L4) substantive hypothesis is derivable in the multiplicative case.**