MultiplicativeRecognizer

formal source

  60positive reals `ℝ_{>0}`, equipped with a continuous comparison operator
  61satisfying the Law of Logic. The structure pairs the geometric recognizer
  62data with the cost-functional data needed to derive (L4) automatically. -/
  63structure MultiplicativeRecognizer (𝒞 : Type*) where
  64  /-- The underlying geometric recognizer onto positive reals. -/
  65  recognizer : Recognizer 𝒞 {x : ℝ // 0 < x}
  66  /-- The continuous comparison operator on positive reals. -/
  67  comparator : ComparisonOperator
  68  /-- The comparator satisfies the Law of Logic (all four Aristotelian
  69      conditions plus scale invariance and non-triviality). -/
  70  laws : SatisfiesLawsOfLogic comparator
  71
  72namespace MultiplicativeRecognizer
  73
  74variable {𝒞 : Type*}
  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)