costCompose_nonneg

formal source

 143
 144/-- **THEOREM: Cost composition preserves non-negativity.**
 145    If a ≥ 0 and b ≥ 0, then a ★ b ≥ 0. -/
 146theorem costCompose_nonneg (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a ★ b := by
 147  unfold costCompose
 148  have h1 : 0 ≤ 2 * a * b := by positivity
 149  have h2 : 0 ≤ 2 * a := by linarith
 150  have h3 : 0 ≤ 2 * b := by linarith
 151  linarith
 152
 153/-- **The factored form**: a ★ b = 2(a+1)(b+1) − 2.
 154    This reveals the monoid structure: if we set A = a+1, B = b+1,
 155    then A ★' B = 2AB − 2, and (A ★' B) + 1 = 2AB − 1. -/
 156theorem costCompose_factored (a b : ℝ) :
 157    a ★ b = 2 * (a + 1) * (b + 1) - 2 := by
 158  unfold costCompose; ring
 159
 160/-- The nonnegative `★`-magma has no identity element. -/
 161theorem costCompose_no_identity :
 162    ¬ ∃ e : ℝ, 0 ≤ e ∧ ∀ a : ℝ, 0 ≤ a → e ★ a = a := by
 163  intro h
 164  rcases h with ⟨e, he_nonneg, he⟩
 165  have h0 : e ★ 0 = 0 := he 0 le_rfl
 166  rw [costCompose_zero_right] at h0
 167  have he0 : e = 0 := by
 168    linarith
 169  have h1 : (0 : ℝ) ★ 1 = 1 := by
 170    simpa [he0] using he 1 (by positivity)
 171  rw [costCompose_zero_left] at h1
 172  norm_num at h1
 173
 174/-- Third-power associativity: the triple `★`-power is unambiguous. -/
 175theorem costCompose_power_assoc (a : ℝ) : (a ★ a) ★ a = a ★ (a ★ a) := by
 176  simpa using (costCompose_flexible a a)