costCompose_right_cancel
plain-language theorem explainer
Right cancellation for the cost composition operation holds when the right operand is nonnegative. Researchers deriving equations in Recognition Science cost algebras would cite this to symmetrize manipulations of the ★ operation. The proof rewrites the hypothesis via commutativity and reduces directly to the left-cancellation lemma.
Claim. Let ★ denote the cost composition operation on the reals. If $b ≥ 0$ and $a_1 ★ b = a_2 ★ b$, then $a_1 = a_2$.
background
The cost composition ★ is the binary operation on ℝ developed in CostAlgebra to encode the Recognition Composition Law (RCL). Its commutativity is given by the upstream theorem costCompose_comm, proved by unfolding the definition and applying ring arithmetic. Left cancellation is supplied by costCompose_left_cancel: for a ≥ 0, a ★ b₁ = a ★ b₂ implies b₁ = b₂, obtained by subtracting the compositions and showing the coefficient 2a + 2 is nonzero.
proof idea
The proof applies costCompose_comm to both sides of the hypothesis, converting a₁ ★ b = a₂ ★ b into b ★ a₁ = b ★ a₂. It then invokes costCompose_left_cancel with the given nonnegativity of b to conclude a₁ = a₂.
why it matters
This theorem supplies the symmetric counterpart to left cancellation, completing the basic algebraic toolkit for cost systems in Recognition Science. It supports equation solving under the RCL and J-cost structures without introducing new hypotheses. No downstream uses are recorded yet, but the result closes a symmetry gap in the algebra module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.