rcl_without_gate
plain-language theorem explainer
This theorem establishes that any consistency combiner P for the J-cost function on positive reals must coincide with the quadratic RCL form 2uv + 2u + 2v on the non-negative quadrant. Recognition Science researchers working on functional-equation derivations of the composition law would cite it to eliminate the right-affine gate hypothesis. The proof is a direct one-line wrapper that invokes the unconditional surjectivity argument already proved in the Unconditional module.
Claim. Let $J$ denote the J-cost function. Suppose $J(xy) + J(x/y) = P(J(x), J(y))$ holds for all positive real $x, y$. Then $P(u, v) = 2uv + 2u + 2v$ for all non-negative real $u, v$.
background
The J-cost is the Recognition Science cost function satisfying the functional equation $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$, known as the Recognition Composition Law. The module RightAffineFromFactorization addresses Gap 4 in the DAlembert factorization chain: whether the combiner $P$ can be forced to the RCL polynomial without assuming right-affine as an independent hypothesis. The local setting is the factorization-plus-associativity approach to deriving the RCL, where earlier modules encoded right-affine as a gate (see ledger_forces_regrouping). This declaration re-exposes the surjectivity route that bypasses the gate entirely by using that $J$ maps onto $[0, ∞)$.
proof idea
The proof is a one-line wrapper that applies Unconditional.rcl_unconditional to the given consistency hypothesis hCons. No additional tactics or reductions are performed inside this module; the surjectivity of J on the non-negative reals and the resulting algebraic identification of P are handled upstream.
why it matters
The result supplies one of the two gate-free routes to the RCL polynomial listed in the module summary, the other being the polynomial-consistency path via bilinear_family_forced. It directly supports the core claim that the Recognition Composition Law does not rest on an unproved right-affine assumption. The declaration touches the remaining open question noted in the module: proving that any consistency combiner must be polynomial from smoothness alone, a step this surjectivity argument deliberately avoids.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.