inner_factor_pos
plain-language theorem explainer
The lemma establishes strict positivity of the quintic 300 + 830t + 924t² + 516t³ + 144t⁴ + 16t⁵ for every nonnegative real t. Researchers proving that only the zero function satisfies a degree-3 d'Alembert-type functional equation cite this algebraic fact. The argument reduces the inequality to nonnegativity of squares of t and its powers via a single non-linear arithmetic tactic.
Claim. For every real number $t$ satisfying $t ≥ 0$, the inequality $300 + 830t + 924t^2 + 516t^3 + 144t^4 + 16t^5 > 0$ holds.
background
The module shows that no continuous nonconstant function G : ℝ → ℝ with G(0) = 0 satisfies the degree-3 composition law G(t + u) + G(t - u) = 2·G(t) + 2·G(u) + G(t)²·G(u) + G(t)·G(u)². This law arises from the symmetric combiner P(s, r) = 2s + 2r + s²r + sr² of total degree 3. Specific substitutions yield polynomial expressions for G(2s), G(3s) and G(4s) in the variable y = G(s). The required identity at the pair (3s, s) produces a degree-9 left-hand side and a degree-15 right-hand side whose difference factors as y^5 times the inner quintic evaluated at t = y².
proof idea
The proof is a one-line wrapper that applies the nlinarith tactic. It supplies the three witnesses sq_nonneg t, sq_nonneg (t * t) and sq_nonneg (t ^ 2) to certify that the quintic cannot reach zero or become negative on the nonnegative reals.
why it matters
The lemma is invoked directly by mismatch_forces_zero to conclude that the full mismatch polynomial 300y^5 + 830y^7 + ⋯ + 16y^15 vanishes only at y = 0. It thereby supplies the algebraic core of the degree-exclusion argument and closes the gap in the d'Alembert Inevitability Theorem: the assumption that the polynomial combiner has degree exactly 2 is forced by the nonexistence of continuous nonconstant solutions for every degree ≥ 3. The degree-counting relation d(d-1)(d-2) > 0 for d ≥ 3 supplies the underlying reason for the mismatch.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.