`cost`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.MultiplicativeRecognizerL4
domain: Foundation
line: 78 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 on GitHub at line 78.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  75
  76/-- The cost function induced by a multiplicative recognizer: the derived
  77cost of its comparator on positive ratios. -/
  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

papers checked against this theorem

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