consistency_forces_RCL_form_is_theorem
plain-language theorem explainer
The theorem establishes that a symmetric quadratic polynomial P satisfying multiplicative consistency with a normalized symmetric cost functional F must take the exact bilinear form 2uv + 2u + 2v once P(1,1) is fixed at 6. Researchers deriving the Recognition Composition Law from first principles would cite this as the normalization step that converts the general bilinear family into the canonical RCL interaction term. The proof obtains the general bilinear coefficients via the upstream inevitability lemma and fixes the cross-term coefficient c
Claim. Let $F: (0,∞) → ℝ$ satisfy $F(x) = F(1/x)$ for $x > 0$, $F(1) = 0$, twice continuous differentiability, and continuity on the positive reals, with $F$ non-constant. Let $P: ℝ × ℝ → ℝ$ be a symmetric quadratic polynomial such that $F(xy) + F(x/y) = P(F(x), F(y))$ for all $x,y > 0$ and $P(1,1) = 6$. Then $P(F(x), F(y)) = 2 F(x) F(y) + 2 F(x) + 2 F(y)$ for all $x,y > 0$.
background
The local setting is the full unconditional RCL inevitability theorem, which assumes only normalization $F(1)=0$, reciprocal symmetry of $F$, $C^2$ smoothness, multiplicative consistency via some $P$, and non-triviality, then forces both $F$ to equal the J-cost $J(x) = (x + x^{-1})/2 - 1$ and $P$ to the bilinear RCL form. The key upstream result is bilinear_family_forced, which states that the consistency requirement forces the unique bilinear family: given normalized symmetric $F$ with multiplicative consistency to a symmetric quadratic polynomial $P$, the form $P(u,v) = a + b u + c v + d u v + e u^2 + f v^2$ is constrained to a specific one-parameter family. This declaration sits inside the DAlembert.FullUnconditional module that completes the forcing chain without prior assumptions on $P$.
proof idea
The proof is a short tactic sequence. It first invokes bilinear_family_forced on the given hypotheses to obtain the general bilinear expression $P(u,v) = 2u + 2v + c u v$. A direct substitution at (1,1) together with the supplied normalization $P(1,1)=6$ yields the linear equation that forces $c=2$ by linarith. The target identity is then recovered by rewriting the consistency equation with this fixed coefficient and simplifying by ring.
why it matters
This is the explicit normalization bridge that converts the polynomial inevitability result into the canonical RCL form required by the full unconditional theorem. It is invoked directly by full_inevitability_explicit and washburn_full_unconditional to finish the argument that both $F$ and $P$ are forced. In the Recognition Science framework it supplies the final step that pins the interaction term of the Recognition Composition Law after the bilinear family is established, advancing the T5 J-uniqueness landmark and the derivation of the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.