costCompose_sub_left
plain-language theorem explainer
Subtracting two cost compositions sharing the left operand factors through the coefficient 2a + 2. Researchers establishing cancellation laws inside the Recognition Science cost algebra would cite this identity. The proof reduces by direct expansion of the costCompose definition followed by ring simplification.
Claim. For real numbers $a, b_1, b_2$, the identity $(a ★ b_1) - (a ★ b_2) = (2a + 2)(b_1 - b_2)$ holds, where the cost composition is the operation $a ★ b := 2ab + 2a + 2b$.
background
Cost composition is the binary operation defined by $a ★ b = 2ab + 2a + 2b$, equivalently $2(a+1)(b+1)-2$. This encodes the Recognition Composition Law on J-costs, where $J(x) = (x + x^{-1})/2 - 1$. The Algebra.CostAlgebra module builds algebraic properties of this operation on top of the cost definitions imported from MultiplicativeRecognizerL4 and ObserverForcing, which extract J-cost from recognition events and multiplicative recognizers.
proof idea
The proof unfolds the costCompose definition on both sides of the difference and applies the ring tactic to verify the resulting polynomial identity.
why it matters
This identity is the direct step used inside costCompose_left_cancel to obtain left cancellation on the nonnegative range, documented there as Equation (2.6). It supplies the algebraic manipulation required for the cost algebra layer of the Recognition Science framework, consistent with the RCL and J-uniqueness from the forcing chain. No open questions or scaffolding are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.