costCompose_no_identity

formal source

 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)
 177
 178/-- Four copies already witness failure of full power-associativity. -/
 179theorem costCompose_fourfold_power_counterexample :
 180    (((1 : ℝ) ★ 1) ★ 1) ★ 1 ≠ ((1 : ℝ) ★ 1) ★ ((1 : ℝ) ★ 1) := by
 181  norm_num [costCompose]
 182
 183/-! ## §4. The Shifted Monoid: H = J + 1 -/
 184
 185/-- The shifted cost: H(x) = J(x) + 1 = ½(x + x⁻¹).
 186    Under H, the RCL becomes the standard d'Alembert equation:
 187    H(xy) + H(x/y) = 2·H(x)·H(y) -/
 188noncomputable def H (x : ℝ) : ℝ := J x + 1
 189
 190/-- H at identity equals 1. -/
 191theorem H_at_one : H 1 = 1 := by