theorem proved term proof

`costCompose_zero_right`

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

formal statement (Lean)

 140theorem costCompose_zero_right (a : ℝ) : a ★ (0 : ℝ) = 2 * a := by

proof body

Term-mode proof.

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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

costCompose_no_identity in IndisputableMonolith.Algebra.CostAlgebra decl_use

depends on (3)

Lean names referenced from this declaration's body.

costCompose in IndisputableMonolith.Algebra.CostAlgebra decl_use
Cost in IndisputableMonolith.Measurement.RSNative.Core decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use