IndisputableMonolith.Foundation.DAlembert.DegreeExclusion
The DegreeExclusion module proves that the inner factor polynomial 300 + 830t + 924t² + 516t³ + 144t⁴ + 16t⁵ remains strictly positive for every t ≥ 0. This forces the mismatch polynomial y⁵ · (inner factor evaluated at t = y²) to vanish only at y = 0. Algebraic researchers working on composition constraints in the d'Alembert setting cite these lemmas to rule out nontrivial degree-3 solutions. The argument proceeds by side expansions followed by direct positivity verification on the inner factor.
claimThe polynomial $p(t) = 300 + 830t + 924t^2 + 516t^3 + 144t^4 + 16t^5$ satisfies $p(t) > 0$ for all real $t ≥ 0$. Consequently the mismatch $y^5 · p(y^2)$ equals zero only when $y = 0$.
background
This module sits inside the Foundation.DAlembert section and supplies the algebraic machinery for degree exclusion. It introduces the inner factor positivity claim together with mismatch_forces_zero, the side expansions lhs_expansion and rhs_expansion, and the ring lemmas doubling_ring, tripling_ring, quadrupling_ring that culminate in no_degree3_composition. The module imports Mathlib.Tactic to carry out the required polynomial identities and sign checks.
proof idea
The module chains a sequence of lemmas. lhs_expansion and rhs_expansion produce the explicit mismatch form. inner_factor_pos verifies the inner factor is positive for t ≥ 0 by direct coefficient inspection. mismatch_forces_zero then concludes the only root occurs at y = 0. The doubling, tripling and quadrupling ring lemmas handle the multiplicative cases that feed no_degree3_composition.
why it matters in Recognition Science
The module supplies the degree-3 exclusion step required by the d'Alembert construction. It directly supports no_degree3_composition and thereby protects uniqueness properties higher in the foundation layer. No downstream theorems are listed in the current graph.
scope and limits
- Does not prove positivity for t < 0.
- Does not treat degrees other than 3.
- Does not supply numerical root bounds beyond the algebraic argument.
- Does not extend the result to complex coefficients.