P_forced_from_FJ
plain-language theorem explainer
If a function F satisfies the multiplicative consistency relation with combiner P and equals the J-cost function, then P must take the explicit RCL form 2uv + 2u + 2v. Researchers closing the Recognition Science forcing chain cite this to finish the d'Alembert gate without extra bridge hypotheses. The proof builds an auxiliary consistency statement for Jcost by substitution and hands it to the unconditional RCL theorem.
Claim. Suppose $F:ℝ→ℝ$ satisfies $F(xy)+F(x/y)=P(F(x),F(y))$ for all positive $x,y$, and $F(x)=J(x)$ for positive $x$ where $J$ is the J-cost function. Then the combiner satisfies $P(u,v)=2uv+2u+2v$ for all nonnegative $u,v$.
background
The J-cost function is the unique solution to the Recognition Composition Law (RCL) given by $J(x)=(x+x^{-1})/2-1$, equivalently cosh(log x)-1. The consistency hypothesis states that the combiner P reproduces the additive structure of F under the multiplicative argument pair (xy,x/y). The module TriangulatedProof assembles four gates (interaction, entanglement, curvature, d'Alembert) that together force any F obeying the consistency relation to be J and P to be RCL.
proof idea
The proof first substitutes the hypothesis F = Jcost into the consistency relation to obtain a matching statement for Jcost. It then applies the upstream lemma rcl_unconditional to that statement, which directly yields the required algebraic form of P.
why it matters
This theorem supplies the final unconditional step in the four-gate inevitability argument, feeding directly into full_inevitability_four_gates. It completes the chain from J-uniqueness (T5) through the RCL to the eight-tick octave and D=3 without requiring the three-gate bridge hypothesis. The result confirms that J passes all four gates while Fquad fails them, closing the triangulated proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.