`costCompose_assoc_defect`

proved

show as: view math explainer →

module: IndisputableMonolith.Algebra.CostAlgebra
domain: Algebra
line: 126 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Algebra.CostAlgebra on GitHub at line 126.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 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. -/
 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 : ℝ) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.