tripling_ring
plain-language theorem explainer
The lemma verifies the algebraic identity obtained by substituting the quadratic expression for G(2s) into the degree-3 combiner P and subtracting G(s), which produces the explicit polynomial 9y + 24y^3 + 18y^5 + 4y^7 for G(3s). Researchers deriving contradictions for continuous nonconstant G with G(0)=0 in functional equations cite this step when checking consistency of the composition law at argument pair (3s,s). The proof is a direct one-line algebraic verification.
Claim. For all real $a$, let $y = a$ and let $G(2s) = 4y + 2y^3$. Then $2(4y + 2y^3) + 2y + (4y + 2y^3)^2 y + (4y + 2y^3) y^2 - y = 9y + 24y^3 + 18y^5 + 4y^7$.
background
The module establishes that no continuous nonconstant function $G : ℝ → ℝ$ with $G(0) = 0$ can satisfy 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$. The symmetric combiner is $P(s,r) = 2s + 2r + s^2 r + s r^2$, which satisfies $P(0,v) = 2v$. From the pair $(s,s)$ one obtains the quadratic $G(2s) = 4y + 2y^3$ where $y = G(s)$. The lemma supplies the next expansion $G(3s) = 9y + 24y^3 + 18y^5 + 4y^7$ required for the consistency check at $(3s,s)$. Upstream results supply the concrete realization $G(t) = J(e^t) = cosh(t) - 1$ in log coordinates together with the identity event at the J-cost minimum.
proof idea
The proof is a one-line wrapper that applies the ring tactic to expand both sides of the polynomial identity and confirm equality after substitution of the quadratic expression for G(2s).
why it matters
The identity is invoked directly by the Degree-3 Exclusion Theorem (no_degree3_composition) to produce the degree mismatch (LHS degree 9 versus RHS degree 15) that forces G identically zero. It closes the gap in the d'Alembert Inevitability Theorem by showing that polynomial combiners of degree ≥ 3 admit no nonconstant continuous solutions, thereby confirming that only the quadratic case is compatible with the Recognition Science forcing chain (T5 J-uniqueness through T8 D=3).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.