mismatch_forces_zero

The module proves that no continuous nonconstant $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$. Substituting the four argument pairs $(s,s)$, $(2s,s)$, $(2s,2s)$ and $(3s,s)$ produces explicit polynomial expressions for $G(2s)$, $G(3s)$ and $G(4s)$ in the variable $y = G(s)$. Their comparison at $(3s,s)$ yields the degree-15 mismatch polynomial whose only real root is zero; the present lemma records that algebraic fact. It depends on the positivity statement that the inner factor $300 + 830t + 924t^2 + 516t^3 + 144t^4 + 16t^5 > 0$ for all $t ≥ 0$ and on the zero-divisor property that a product of reals is zero only if at least one factor is zero.

Rewrite the hypothesis by nlinarith as $a^5$ times the inner quintic in $a^2$ equals zero. Apply inner_factor_pos to the non-negative quantity $a^2$ to obtain strict positivity of the second factor. Invoke mul_eq_zero on the product to split into the two cases $a^5 = 0$ or inner factor = 0; the second case is impossible by positivity, so $a^5 = 0$. Conclude $a = 0$ from the fact that the exponent 5 is nonzero.

The lemma supplies the contradiction that forces every solution of the degree-3 law to be identically zero, thereby discharging the parent theorem no_degree3_composition. That theorem in turn closes the gap in the d'Alembert Inevitability argument by showing that any polynomial combiner of total degree ≥ 3 produces an irreconcilable degree mismatch between the two sides of the functional equation. Within Recognition Science the result therefore enforces that the only admissible combiner is the quadratic one compatible with the self-similar fixed point at T6 and the eight-tick octave at T7.