RCL_holds
plain-language theorem explainer
J(x) = (x + x^{-1})/2 - 1 satisfies the Recognition Composition Law J(xy) + J(x/y) = 2 J(x) J(y) + 2 J(x) + 2 J(y) for all positive reals x and y. Recognition Science researchers cite this verification when assembling the canonical cost algebra from the primitive identity. The proof is a direct term-mode algebraic check: positivity assumptions clear denominators via field_simp, after which ring normalizes the identity.
Claim. $J(x) = (x + x^{-1})/2 - 1$ satisfies $J(xy) + J(x/y) = 2 J(x) J(y) + 2 J(x) + 2 J(y)$ for all $x, y > 0$.
background
The Recognition Composition Law is the single primitive of the framework: a function F satisfies it when F(xy) + F(x/y) = 2 F(x) F(y) + 2 F(x) + 2 F(y) holds for positive arguments. This is the multiplicative form of the d'Alembert equation stated as the Composition axiom in CostAxioms. The J-cost is the explicit function J(x) = (x + x^{-1})/2 - 1, introduced in the module as the normalized cost obeying this law. The CostAlgebra module builds the induced algebraic structure on costs, including composition, associator defects, and the canonical data package.
proof idea
The term proof introduces positive x and y, derives the four nonzeroness facts for x, y, xy, and x/y, unfolds J to its explicit rational form, applies field_simp to clear all denominators, and finishes with ring to confirm the resulting polynomial identity.
why it matters
RCL_holds supplies the rcl field for canonicalCostAlgebra and canonicalRecognitionCostSystem, and appears inside the cost_algebra_certificate that lists the five core properties of J. It confirms the foundational identity required by the Recognition Composition Law, directly supporting the forcing chain from the Composition axiom through J-uniqueness to the phi-ladder and eight-tick octave. No open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.