no_degree3_composition
plain-language theorem explainer
Any real-valued function G satisfying the degree-3 functional equation G(t+u)+G(t-u)=2G(t)+2G(u)+G(t)^2 G(u)+G(t)G(u)^2 with G(0)=0 must be identically zero. Researchers proving the d'Alembert inevitability theorem in Recognition Science cite this to rule out higher-degree combiners. The proof derives explicit polynomials for G(2s), G(3s), G(4s) in terms of G(s), substitutes into the equation at (3s,s), and shows the resulting mismatch polynomial vanishes only at zero.
Claim. Let $G : ℝ → ℝ$ satisfy $G(t+u) + G(t-u) = 2G(t) + 2G(u) + G(t)^2 G(u) + G(t) G(u)^2$ for all real $t,u$ with $G(0)=0$. Then $G(s)=0$ for every real $s$.
background
The module proves exclusion of degree ≥3 polynomial combiners for the d'Alembert equation. The symmetric combiner is P(s,r)=2s+2r+s²r+sr², which satisfies P(0,v)=2v and has total degree 3. Upstream lemmas supply the ring identities: doubling_ring states P(y,y)=4y+2y³; tripling_ring and quadrupling_ring give the corresponding expansions for G(3s) and G(4s) as polynomials in y=G(s). The module documentation records the explicit forms G(2s)=4y+2y³, G(3s)=9y+24y³+18y⁵+4y⁷, G(4s)=16y+136y³+192y⁵+96y⁷+16y⁹.
proof idea
Apply the functional equation at (s,s) and invoke doubling_ring to obtain G(2s)=4a+2a³ (a=G(s)). Use the equation at (2s,s) together with tripling_ring to express G(3s) as a degree-7 polynomial. Apply the equation at (2s,2s) with quadrupling_ring to obtain G(4s) as a degree-9 polynomial. Substitute these into the equation at (3s,s), then apply lhs_expansion and rhs_expansion to produce the mismatch polynomial 300a⁵+830a⁷+…+16a¹⁵=0. Finally invoke mismatch_forces_zero to conclude a=0.
why it matters
This theorem shows that no nonconstant continuous solution exists for any degree-3 polynomial combiner, thereby closing the gap in the d'Alembert Inevitability Theorem: the degree-2 assumption is forced rather than extra. The module documentation states that the degree mismatch deg(LHS)=d² versus deg(RHS)=d³-2d²+2d is positive for all d≥3, ruling out higher-degree cases. In the Recognition Science setting this supports the uniqueness of the composition law derived from the forcing chain (T0-T8) and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.