costCompose_factored
plain-language theorem explainer
Cost composition under the Recognition Composition Law satisfies a ★ b = 2(a + 1)(b + 1) − 2 for real a, b. Researchers deriving monoid structure from J-costs in Recognition Science cite this to shift variables and expose multiplicative closure. The proof is a one-line wrapper that unfolds the costCompose definition and normalizes via ring arithmetic.
Claim. For all real numbers $a, b$, the cost composition operation satisfies $a ★ b = 2(a + 1)(b + 1) - 2$, where ★ is the binary operation induced by the Recognition Composition Law on J-cost levels.
background
In the CostAlgebra module the binary operation ★ is defined by costCompose(a, b) := 2ab + 2a + 2b. This operation is induced directly by the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y), with J the unique cost function J(x) = (x + x^{-1})/2 − 1. The upstream costCompose declaration records the expanded form and notes that it equals 2(a + 1)(b + 1) − 2 after algebraic rearrangement.
proof idea
The proof is a one-line wrapper that applies the definition of costCompose and invokes the ring tactic to equate 2ab + 2a + 2b with the factored expression 2(a + 1)(b + 1) − 2.
why it matters
The factored identity supplies the change of variables A = a + 1, B = b + 1 that converts ★ into the monoid operation A ★' B = 2AB − 2. It therefore supports algebraic closure arguments inside the Recognition framework and sits between the RCL and later monoid or associativity results. No downstream uses are recorded yet, but the declaration closes the algebraic simplification step required by the cost-composition construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.