costCompose_right_cancel
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.
claimLet ★ 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 in Recognition Science
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.
scope and limits
- Does not establish cancellation when the right operand is negative.
- Does not prove associativity of ★.
- Does not derive an explicit closed-form expression for the composition.
- Does not address uniqueness outside the cancellation setting.
formal statement (Lean)
509theorem costCompose_right_cancel {a₁ a₂ b : ℝ} (hb : 0 ≤ b)
510 (h : a₁ ★ b = a₂ ★ b) : a₁ = a₂ := by
proof body
Term-mode proof.
511 rw [costCompose_comm a₁ b, costCompose_comm a₂ b] at h
512 exact costCompose_left_cancel hb h
513
514/-! ## §5b. Recognition Cost Systems and Window Aggregation -/
515
516/-- The ambient domain of recognition cost systems: positive reals. -/