consistency_forces_RCL_polynomial
plain-language theorem explainer
Given that F equals the J-cost function and obeys the d'Alembert consistency relation with a pairing P, the theorem forces P to equal the explicit form 2uv + 2u + 2v on the non-negative reals. Workers deriving the Recognition Science functional equation from first principles would invoke this result to pin down the polynomial structure of the composition law. The proof lifts each pair (u,v) to preimages under the surjective map F, substitutes into the consistency equation, and reduces via the known RCL identity for J.
Claim. Assume $F:ℝ→ℝ$ and $P:ℝ→ℝ→ℝ$ satisfy $F(x)=F(x^{-1})$ for all $x>0$, $F(1)=0$, $F$ is $C^2$, the uncurried $P$ is $C^2$, the consistency relation $F(xy)+F(x/y)=P(F(x),F(y))$ for $x,y>0$, $F$ surjects onto $[0,∞)$, and $F(x)=J(x)$ for $x>0$ where $J(x)=(x+x^{-1})/2-1$. Then $P(u,v)=2uv+2u+2v$ for all $u,v≥0$.
background
The module proves the strongest form of RCL inevitability: both F and P are forced with no assumption on P. The J-cost function is defined by $J(x)=(x+x^{-1})/2-1$, equivalently cosh(log x)-1, and satisfies the Recognition Composition Law. The consistency hypothesis states that F(xy)+F(x/y) equals P of the images under F for positive x,y. This result sits inside the FullUnconditional development, which assumes only normalization at 1, reciprocal symmetry, C² smoothness, and existence of some P satisfying the multiplicative consistency equation. The upstream lemma J_computes_P records the explicit RCL identity satisfied by J itself: J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y).
proof idea
The argument lifts arbitrary non-negative u and v to positive preimages x and y via the surjectivity hypothesis on F. It substitutes into the consistency relation to express P(u,v) as F(xy)+F(x/y), replaces F by J using the identification hypothesis, and invokes the known RCL identity J_computes_P to obtain the bilinear expression. The final step applies linarith after rewriting the images under J.
why it matters
This lemma completes the computation of P once F has been identified with J, thereby finishing the unconditional forcing argument in the FullUnconditional module. It directly supports the claim that P must be the specific quadratic form 2uv+2u+2v. Within the Recognition Science framework it closes the step from J-uniqueness (T5) to the explicit RCL polynomial, consistent with the eight-tick octave and the derivation of spatial dimension D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.