P_uniqueness
plain-language theorem explainer
Any two functions P and Q that each reproduce the J-cost consistency relation on positive reals must agree on the non-negative quadrant. Recognition Science derivations cite this result to exclude all alternative forms for the auxiliary function in the composition law. The argument applies the unconditional determination lemma separately to each hypothesis and equates the resulting explicit expressions.
Claim. Let $J$ denote the J-cost function. Suppose $P$ and $Q$ each satisfy $J(xy) + J(x/y) = P(J(x), J(y))$ for all $x, y > 0$. Then $P(u, v) = Q(u, v)$ for all $u, v ≥ 0$.
background
The J-cost function satisfies $J(x) = (x + x^{-1})/2 - 1$, or equivalently $J(x) = cosh(log x) - 1$. The Recognition Composition Law states $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$. This module proves unconditional inevitability of the RCL: no assumption on the auxiliary function P is required beyond the existence of some F obeying symmetry, normalization, calibration, smoothness, and multiplicative consistency with P. Then F equals J by ODE uniqueness and P is computed directly from the equation applied to J.
proof idea
The proof introduces arbitrary non-negative u and v. It applies the upstream lemma rcl_unconditional to the hypothesis for P, obtaining the explicit bilinear form on the first quadrant. The same lemma is applied to the hypothesis for Q. Rewriting equates the two sides.
why it matters
This uniqueness result confirms that the RCL is the only consistency relation compatible with J-cost, ruling out polynomial and irregular alternatives. It completes the Unconditional RCL Inevitability argument in the module and supports the forcing chain from T5 J-uniqueness through T8 D=3. The theorem feeds into sibling results such as complete_forcing_chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.