theorem proved tactic proof

`costCompose_nonneg`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

Last generation error: xAI API error (429): The model is currently at capacity due to high demand. Please try again in a few minutes. For guaranteed processing and availability, please request Provisioned Throughput: https://docs.x.ai/developers/advanced-api-usage/provisioned-throughput

generate prose now

formal statement (Lean)

 146theorem costCompose_nonneg (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a ★ b := by

proof body

Tactic-mode proof.

 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. -/

depends on (5)

Lean names referenced from this declaration's body.

costCompose in IndisputableMonolith.Algebra.CostAlgebra decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use