costCompose_left_cancel
Left cancellation for the cost composition operation holds on the nonnegative range for the left operand. Researchers establishing uniqueness properties in Recognition Science cost systems cite this to support algebraic well-definedness. The proof converts the equality to a zero difference, factors it via the subtraction identity, confirms the coefficient is nonzero, and applies the zero-divisor property to conclude the right operands match.
claimLet $a, b_1, b_2$ be real numbers with $a$ nonnegative. If $a$ composed with $b_1$ equals $a$ composed with $b_2$, then $b_1 = b_2$, where the composition satisfies the difference identity $a$ composed with $b_1$ minus $a$ composed with $b_2$ equals $(2a + 2)$ times $(b_1 - b_2)$.
background
The cost composition operation on real numbers is introduced in the CostAlgebra module as the binary operation satisfying the Recognition Composition Law derived from the J-cost function, with J normalized so that J(1) equals zero and J nonnegative on the positive reals. The subtraction identity factors differences of composed costs through the coefficient 2a + 2, obtained by direct expansion of the operation definition. This theorem sits in the algebraic layer that packages J properties together with the primitive distinction axioms and phi-forcing structures from the foundation modules.
proof idea
The proof begins by rewriting the equality hypothesis as a zero difference via sub_eq_zero. It then invokes the upstream subtraction lemma to replace the difference with the factored form (2a + 2) times (b1 minus b2). A linarith step confirms the coefficient 2a + 2 is nonzero under the nonnegativity assumption on a. The mul_eq_zero theorem splits the product being zero into cases, eliminates the coefficient-zero case, and reduces to b1 minus b2 equals zero, which linarith resolves.
why it matters in Recognition Science
This cancellation property feeds directly into the cost algebra certificate, which assembles the full list of J properties including RCL satisfaction, normalization, reciprocal symmetry, nonnegativity, and explicit associator defect control. It supplies the left-cancellation step required for the cost algebra to support downstream uniqueness arguments in the Recognition framework, aligning with the forcing chain steps that derive J-uniqueness and the eight-tick octave structure. The result closes one algebraic prerequisite for the paper's equation (2.6) on cost-range cancellation.
scope and limits
- Does not establish cancellation when the left operand is negative.
- Does not provide the explicit closed-form definition of the composition operation.
- Does not address right-cancellation without invoking commutativity separately.
- Does not extend the result to non-real scalars or higher-dimensional costs.
Lean usage
example {a b1 b2 : ℝ} (ha : 0 ≤ a) (h : a ★ b1 = a ★ b2) : b1 = b2 := costCompose_left_cancel ha hformal statement (Lean)
496theorem costCompose_left_cancel {a b₁ b₂ : ℝ} (ha : 0 ≤ a)
497 (h : a ★ b₁ = a ★ b₂) : b₁ = b₂ := by
proof body
Tactic-mode proof.
498 have hsub : a ★ b₁ - a ★ b₂ = 0 := sub_eq_zero.mpr h
499 rw [costCompose_sub_left] at hsub
500 have hcoeff : 2 * a + 2 ≠ 0 := by
501 linarith
502 have hdiff : b₁ - b₂ = 0 := by
503 rcases mul_eq_zero.mp hsub with hzero | hzero
504 · exact False.elim (hcoeff hzero)
505 · exact hzero
506 linarith
507
508/-- Right-cancellation follows from commutativity of `★`. -/