rcl_unconditional
plain-language theorem explainer
Any P satisfying the multiplicative consistency relation with Jcost on positive reals must equal the bilinear expression 2uv + 2u + 2v on the non-negative quadrant. Foundation researchers cite this result to rule out irregular solutions for the comparison equation without assuming polynomial form for P. The argument is a direct reduction to the prior non-negative determination lemma via surjectivity of J onto [0, ∞).
Claim. Let $J$ denote the J-cost function. Suppose $P : ℝ → ℝ → ℝ$ satisfies $∀ x,y > 0$, $J(xy) + J(x/y) = P(J(x), J(y))$. Then $∀ u,v ≥ 0$, $P(u,v) = 2uv + 2u + 2v$.
background
The module proves unconditional inevitability of the Recognition Composition Law. The J-cost function satisfies symmetry J(x) = J(1/x), normalization J(1) = 0, calibration via second derivative of the log-variable form, and smoothness. Multiplicative consistency states that J(xy) + J(x/y) equals P applied to the pair (J(x), J(y)) for some auxiliary function P, with no further restriction on P's shape. Upstream, P_determined_nonneg establishes the same conclusion on [0, ∞)² by invoking surjectivity of J onto the non-negative reals.
proof idea
One-line wrapper that applies P_determined_nonneg to the given consistency hypothesis.
why it matters
This declaration supplies the gate-free form of RCL used by rcl_without_gate and by ultimate_inevitability in the DAlembert.Ultimate module. It realizes the T5 J-uniqueness step and the Recognition Composition Law without any polynomial hypothesis on P. The result closes the mathematician's concern about irregular solutions by computing P directly from the functional equation once F is fixed as J.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.