polynomial_form_forced
plain-language theorem explainer
The theorem establishes that any symmetric quadratic polynomial P satisfying the normalization P(0, v) = 2v for all v, together with P(0,0) = 0 and a non-triviality condition, must reduce to the bilinear form 2u + 2v + k uv. Researchers deriving the uniqueness of the d'Alembert equation from cost-functional consistency in Recognition Science would cite this when closing the gap between arbitrary polynomials and the required multiplicative structure. The proof works by direct coefficient extraction from the general quadratic, followed by linear-
Claim. Let $P : ℝ → ℝ → ℝ$ be a polynomial of degree at most two. Suppose $P$ is symmetric ($P(u,v) = P(v,u)$ for all $u,v$), satisfies the normalization $P(0,v) = 2v$ for all $v$, and obeys $P(0,0) = 0$. If $P$ is non-trivial (i.e., $P(u_0,v_0) ≠ 2u_0 + 2v_0$ for some $u_0,v_0$), then there exists a real constant $k$ such that $P(u,v) = 2u + 2v + k uv$ for all $u,v$.
background
In the D'Alembert Equation Inevitability module the goal is to show that the d'Alembert functional equation is the unique form compatible with multiplicative consistency of a cost functional. A cost functional $F$ obeys symmetry $F(x) = F(1/x)$, normalization $F(1) = 0$, and the consistency relation $F(xy) + F(x/y) = P(F(x), F(y))$ where $P$ is required to be a symmetric quadratic polynomial. The shifted cost $H(x) = J(x) + 1$ (from CostAlgebra) converts this relation into the standard d'Alembert equation $H(xy) + H(x/y) = 2 H(x) H(y)$.
proof idea
The proof obtains the six coefficients from the polynomial assumption, then substitutes the normalization $P(0,v) = 2v$ at the points $v = 0,1,2$ to force $a = 0$, $c = 2$, $f = 0$ by solving the resulting linear system with linarith. Symmetry is applied at the swapped points $(1,0)$ and $(2,0)$ to force $b = 2$ and $e = 0$ by the same coefficient comparison. The remaining coefficient $d$ is taken as $k$ and the identity is verified by substitution and ring simplification.
why it matters
This supplies the precise polynomial shape required by the parent theorem bilinear_family_forced, which states that any cost functional obeying the listed axioms must satisfy the bilinear family $P(u,v) = 2u + 2v + k uv$. In the Recognition Science framework it completes the proof that the Recognition Composition Law is inevitable rather than postulated, thereby closing the transcendental argument for the axiom bundle A1–A3. The result directly supports the claim that the consistency equation reduces to d'Alembert after the affine shift $H(t) = 1 + (c/2)G(t)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.