SatisfiesRCL
plain-language theorem explainer
The Recognition Composition Law is the single primitive functional equation of Recognition Science, requiring any cost function F to obey F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y) for positive reals x and y. Researchers building cost algebras or deriving the J-cost cite this definition as the starting algebraic interface. It is introduced directly as a Prop without reduction or additional hypotheses.
Claim. A function $F : (0, +∞) → ℝ$ satisfies the Recognition Composition Law if for all $x, y > 0$, $F(xy) + F(x/y) = 2 F(x) F(y) + 2 F(x) + 2 F(y)$.
background
The J-cost is the function $J(x) = ½(x + x^{-1}) - 1$, introduced as the unique cost obeying the Recognition Composition Law. In log coordinates $t = ln x$, $u = ln y$ the equation becomes the calibrated multiplicative d'Alembert form $G(t+u) + G(t-u) = 2G(t)G(u) + 2(G(t) + G(u))$. The CostAlgebra module packages this law together with normalization at the identity event (J(1) = 0) and reciprocal symmetry, drawing on the canonical identity from ObserverForcing.
proof idea
This is the direct definition of the property; the body is the universal quantification over positive reals exactly as stated in the doc-comment.
why it matters
SatisfiesRCL is the core primitive that feeds the cost_algebra_certificate (which verifies J obeys RCL plus normalization, symmetry and non-negativity) and the CostAlgebraData structure. It is the ONE primitive of Recognition Science from which the forcing chain (T5 J-uniqueness onward) and all downstream cost systems derive; the RCL_holds theorem then shows J itself satisfies the property.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.