tripling_ring
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.
claimFor 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 in Recognition Science
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).
scope and limits
- Does not prove existence of any non-trivial solutions to the functional equation.
- Does not apply when G is discontinuous.
- Does not address combiners whose total degree differs from 3.
- Does not cover the case G(0) ≠ 0.
formal statement (Lean)
94lemma tripling_ring (a : ℝ) :
95 2 * (4 * a + 2 * a ^ 3) + 2 * a +
96 (4 * a + 2 * a ^ 3) ^ 2 * a + (4 * a + 2 * a ^ 3) * a ^ 2 - a =
97 9 * a + 24 * a ^ 3 + 18 * a ^ 5 + 4 * a ^ 7 := by ring
proof body
Term-mode proof.
98
99/-- **Ring identity (G(4s))**: Expanding `P(G(2s), G(2s))`. -/