SatisfiesRCL
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not assert that any concrete function satisfies the law.
- Does not derive the closed form of J.
- Does not include normalization J(1) = 0 or non-negativity.
- Does not address the log-coordinate d'Alembert rewriting.
formal statement (Lean)
92def SatisfiesRCL (F : ℝ → ℝ) : Prop :=
proof body
Definition body.
93 ∀ x y : ℝ, 0 < x → 0 < y →
94 F (x * y) + F (x / y) = 2 * F x * F y + 2 * F x + 2 * F y
95
96/-- **THEOREM: J satisfies the RCL.**
97 This is the foundational identity — everything else follows. -/