99 intro x y hx hy 100 unfold J Jcost 101 have hx0 : x ≠ 0 := ne_of_gt hx 102 have hy0 : y ≠ 0 := ne_of_gt hy 103 have hxy0 : x * y ≠ 0 := mul_ne_zero hx0 hy0 104 have hxy_div0 : x / y ≠ 0 := div_ne_zero hx0 hy0 105 field_simp [hx0, hy0, hxy0, hxy_div0] 106 ring 107 108/-! ## §3. Cost Composition as Algebraic Operation -/ 109 110/-- **Cost-composition**: The binary operation on costs induced by the RCL. 111 Given two "cost levels" a = J(x) and b = J(y), the composed cost is: 112 a ★ b = 2ab + 2a + 2b = 2(a+1)(b+1) − 2 113 114 This captures how costs combine under multiplication of ratios. -/
used by (5)
From the project-wide theorem graph. These declarations reference this one in their body.