doubling_ring
plain-language theorem explainer
The algebraic identity P(y,y) = 4y + 2y³ holds for the symmetric degree-3 combiner P(s,r) = 2s + 2r + s²r + sr². Analysts deriving forced doubling maps inside functional equations for continuous G with G(0)=0 would invoke this step when building the contradiction for degree-3 laws. The proof is a direct one-line wrapper that applies the ring tactic to equate the expanded polynomials.
Claim. For the symmetric polynomial combiner defined by $P(s,r) = 2s + 2r + s^2 r + s r^2$, the specialization at equal arguments satisfies $P(y,y) = 4y + 2y^3$ identically.
background
The module establishes that no continuous nonconstant function $G:ℝ→ℝ$ with $G(0)=0$ can obey the degree-3 composition law $G(t+u)+G(t-u)=2G(t)+2G(u)+G(t)^2 G(u)+G(t)G(u)^2$. This law is realized by the symmetric combiner $P(s,r)=2s+2r+s^2 r + s r^2$ of total degree 3, which satisfies $P(0,v)=2v$. The doubling_ring lemma supplies the explicit doubling map obtained by substituting $t=u=s$ into the functional equation, yielding $G(2s)$ as a cubic polynomial in $y=G(s)$.
proof idea
The proof is a one-line wrapper that applies the ring tactic to expand both sides of the target equality in the indeterminate a and confirm they are identical as polynomials.
why it matters
The lemma is invoked inside the proof of the Degree-3 Exclusion Theorem (no_degree3_composition), which concludes that every solution is identically zero. It supplies the first explicit polynomial in the chain that produces G(2s), G(3s) and G(4s), enabling the degree-mismatch argument at the (3s,s) instance. Within the Recognition Science framework this step closes the d'Alembert Inevitability Theorem by showing that the degree-2 assumption on the combiner is forced rather than postulated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.