consistency_forces_RCL_form_hypothesis
plain-language theorem explainer
The declaration encodes the proposition that symmetry under inversion, normalization F(1)=0, C² smoothness of F, and existence of any P satisfying the multiplicative consistency equation together force P to take the bilinear form 2uv + 2u + 2v on the image of F. Researchers closing the unconditional derivation of the Recognition Composition Law cite this step when no prior form is assumed for P. The statement is obtained by twice differentiating the functional equation and substituting the listed boundary conditions.
Claim. Suppose $F: (0,∞) → ℝ$ satisfies $F(x) = F(x^{-1})$, $F(1) = 0$, and $F ∈ C²$. If there exists $P: ℝ → ℝ → ℝ$ such that $F(xy) + F(x/y) = P(F(x), F(y))$ for all $x,y > 0$, then $P(u,v) = 2uv + 2u + 2v$ for all $u,v$ in the range of $F$.
background
This definition sits inside the Full Unconditional RCL Inevitability module, which shows both the cost function and the pairing function are forced with no assumption on P. It uses the J-cost J(x) = (x + x^{-1})/2 - 1 that obeys the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). The local setting is the d'Alembert equation on the positive reals equipped with reciprocal symmetry and C² regularity.
proof idea
The declaration is a direct definition of the stated proposition. The supporting argument differentiates the functional equation twice, evaluates at the normalization point F(1)=0, and solves the resulting linear system for the coefficients of P using symmetry.
why it matters
The proposition is packaged into the FullUnconditionalHypotheses structure that supports the full unconditional inevitability theorem. It supplies the missing link from d'Alembert forcing of the cosh form to the explicit RCL pairing, consistent with T5 J-uniqueness and the eight-tick octave. It leaves open whether C² can be relaxed to C¹ while preserving uniqueness of P.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.