SatisfiesRCL

formal source

  89    G(t+u) + G(t−u) = 2·G(t)·G(u) + 2·(G(t) + G(u))
  90
  91    which is a calibrated multiplicative form of the d'Alembert functional equation. -/
  92def SatisfiesRCL (F : ℝ → ℝ) : Prop :=
  93  ∀ x y : ℝ, 0 < x → 0 < y →
  94    F (x * y) + F (x / y) = 2 * F x * F y + 2 * F x + 2 * F y
  95
  96/-- **THEOREM: J satisfies the RCL.**
  97    This is the foundational identity — everything else follows. -/
  98theorem RCL_holds : SatisfiesRCL J := by
  99  intro x y hx hy
 100  unfold J Jcost
 101  have hx0 : x ≠ 0 := ne_of_gt hx
 102  have hy0 : y ≠ 0 := ne_of_gt hy
 103  have hxy0 : x * y ≠ 0 := mul_ne_zero hx0 hy0
 104  have hxy_div0 : x / y ≠ 0 := div_ne_zero hx0 hy0
 105  field_simp [hx0, hy0, hxy0, hxy_div0]
 106  ring
 107
 108/-! ## §3. Cost Composition as Algebraic Operation -/
 109
 110/-- **Cost-composition**: The binary operation on costs induced by the RCL.
 111    Given two "cost levels" a = J(x) and b = J(y), the composed cost is:
 112    a ★ b = 2ab + 2a + 2b = 2(a+1)(b+1) − 2
 113
 114    This captures how costs combine under multiplication of ratios. -/
 115noncomputable def costCompose (a b : ℝ) : ℝ := 2 * a * b + 2 * a + 2 * b
 116
 117/-- Notation for cost composition -/
 118infixl:70 " ★ " => costCompose
 119
 120/-- **THEOREM: Cost composition is commutative.** -/
 121theorem costCompose_comm (a b : ℝ) : a ★ b = b ★ a := by
 122  unfold costCompose; ring