quadrupling_ring
plain-language theorem explainer
The lemma computes the explicit degree-9 polynomial for G(4s) obtained by applying the degree-3 combiner P twice to G(2s). Researchers deriving contradictions in functional equations for Recognition Science cite this identity when closing the degree-3 case. The proof is a direct term-mode invocation of the ring tactic that expands and equates the two sides.
Claim. Let $y = G(s)$. With $G(2s) = 4y + 2y^3$ and the combiner $P(x,y) = 2x + 2y + x^2 y + x y^2$, the identity asserts $P(G(2s),G(2s)) = 16y + 136y^3 + 192y^5 + 96y^7 + 16y^9$.
background
The module proves that no continuous nonconstant $G:ℝ→ℝ$ with $G(0)=0$ satisfies the degree-3 composition law $G(t+u)+G(t-u)=2G(t)+2G(u)+G(t)^2G(u)+G(t)G(u)^2$. The symmetric combiner is $P(s,r)=2s+2r+s^2r+sr^2$, which satisfies $P(0,v)=2v$. Iterates are obtained by substituting specific pairs: $(s,s)$ yields $G(2s)=4y+2y^3$ with $y=G(s)$; $(2s,2s)$ then yields the degree-9 expression for $G(4s)$. Upstream ledger factorization supplies the calibration of the cost function $J$ whose fixed-point properties motivate the form of $P$.
proof idea
One-line wrapper that applies the ring tactic to expand the left-hand side $2(4a+2a^3)+2(4a+2a^3)+(4a+2a^3)^2(4a+2a^3)+(4a+2a^3)(4a+2a^3)^2$ and confirm equality with the right-hand side polynomial of degree 9.
why it matters
The identity supplies the explicit $G(4s)$ polynomial required by the parent theorem no_degree3_composition, which concludes that every solution of the degree-3 law is identically zero. This step closes the gap in the d'Alembert Inevitability Theorem: the quadratic combiner is forced rather than assumed, consistent with the Recognition Science forcing chain that selects the unique $J$-cost of degree 2. The degree mismatch (LHS degree 9 versus RHS degree 15 at the next step) is the concrete mechanism that excludes all $d≥3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.