costCompose_assoc_defect
plain-language theorem explainer
The associator defect theorem shows that raw cost composition under the Recognition Composition Law fails strict associativity with explicit linear defect 2(a-c). Algebraists assembling the cost algebra package would cite this to confirm controlled non-associativity before normalization steps. The proof is a direct algebraic expansion of the binary operation followed by ring normalization.
Claim. For all real numbers $a,b,c$, the cost composition satisfies $(a ★ b) ★ c = a ★ (b ★ c) + 2(a - c)$, where the 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 on real-valued costs (i.e., images under the J-function). Its definition is costCompose a b = 2ab + 2a + 2b, equivalently 2(a+1)(b+1)-2, which encodes how J-values combine under ratio multiplication. The module already records that this operation is commutative and that J itself satisfies RCL together with J(1)=0, reciprocity, and non-negativity.
proof idea
The term proof unfolds the costCompose definition on both sides of the target equation, then applies ring_nf to reduce the resulting polynomials and confirm that their difference is exactly 2*(a-c).
why it matters
This result supplies the explicit associator defect required by the downstream cost_algebra_certificate, which lists commutativity with controlled defect as one of the five verified properties of the cost algebra. It is also invoked directly to prove the sibling flexibility statement costCompose_flexible. Within the Recognition framework the controlled defect is consistent with the raw RCL before any normalization that recovers stricter algebraic structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.