costCompose_zero_right
plain-language theorem explainer
The cost composition operation satisfies a ★ 0 = 2a for any real a. Algebraists deriving the structure of the nonnegative cost magma in Recognition Science cite this when proving absence of an identity element. The proof is a one-line wrapper that unfolds the costCompose definition and normalizes the resulting polynomial via ring tactics.
Claim. For any real number $a$, $a ★ 0 = 2a$, where the binary operation is defined by $a ★ b := 2ab + 2a + 2b$.
background
In the CostAlgebra module the binary operation ★ is the cost composition induced by the Recognition Composition Law. Its definition is $a ★ b = 2ab + 2a + 2b$, equivalently $2(a+1)(b+1)-2$, which encodes how J-costs combine under ratio multiplication. The Cost type is an abbreviation for Quantity CostUnit. This identity is a direct algebraic consequence of that definition and the ring axioms on the reals.
proof idea
The proof is a one-line wrapper: unfold costCompose followed by ring_nf. These steps substitute the explicit polynomial 2a0 + 2a + 20 and reduce it to 2*a by standard ring simplification.
why it matters
The result is invoked directly in the downstream theorem costCompose_no_identity to derive a contradiction when assuming an identity element exists in the nonnegative ★-magma. It supplies a basic algebraic fact required by the Recognition Science treatment of cost composition arising from the RCL, supporting the larger derivation of the forcing chain (T0-T8) and the absence of trivial units in the cost structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.