costCompose

formal source

 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
 123
 124/-- **THEOREM: Associator defect for raw RCL composition.**
 125    The unnormalized RCL form is not strictly associative; the defect is `2*(a-c)`. -/
 126theorem costCompose_assoc_defect (a b c : ℝ) :
 127    (a ★ b) ★ c = a ★ (b ★ c) + 2 * (a - c) := by
 128  unfold costCompose
 129  ring_nf
 130
 131/-- The raw `★`-operation is flexible. -/
 132theorem costCompose_flexible (a b : ℝ) : (a ★ b) ★ a = a ★ (b ★ a) := by
 133  simpa using (costCompose_assoc_defect a b a)
 134
 135/-- **THEOREM: Left-zero evaluation for raw RCL composition.** -/
 136theorem costCompose_zero_left (a : ℝ) : (0 : ℝ) ★ a = 2 * a := by
 137  unfold costCompose
 138  ring_nf
 139
 140theorem costCompose_zero_right (a : ℝ) : a ★ (0 : ℝ) = 2 * a := by
 141  unfold costCompose
 142  ring_nf
 143
 144/-- **THEOREM: Cost composition preserves non-negativity.**
 145    If a ≥ 0 and b ≥ 0, then a ★ b ≥ 0. -/