IndisputableMonolith.Foundation.DAlembert.DegreeExclusion
The DegreeExclusion module proves that the quintic inner factor 300 + 830t + 924t² + 516t³ + 144t⁴ + 16t⁵ stays strictly positive for all t ≥ 0. This forces the mismatch polynomial y⁵ · f(y²) to vanish only at y = 0. Researchers handling algebraic identities in the Recognition framework cite these results when excluding nontrivial polynomial solutions. The argument uses direct positivity checks together with targeted polynomial expansions and ring lemmas.
claimLet $f(t) = 300 + 830t + 924t^2 + 516t^3 + 144t^4 + 16t^5$. Then $f(t) > 0$ for every $t \geq 0$, which implies that the mismatch polynomial $y^5 \cdot f(y^2)$ has no real root except $y = 0$.
background
The module belongs to the DAlembert subsection of the Foundation layer and supplies algebraic tools for degree exclusion in polynomial compositions. Its central object is the inner factor whose strict positivity is stated in the module doc-comment; this factor appears inside a mismatch polynomial constructed from the Recognition Composition Law. Supporting lemmas expand left- and right-hand sides and establish closure under doubling, tripling, and quadrupling operations. The single import is Mathlib.Tactic, indicating that the proofs rely on automated algebraic simplification rather than external analytic results.
proof idea
The module structures its argument as a linear chain of lemmas. inner_factor_pos verifies positivity of the given quintic by direct evaluation or derivative analysis. mismatch_forces_zero applies that positivity to conclude the mismatch vanishes only at zero. lhs_expansion and rhs_expansion supply the explicit polynomial forms. The ring lemmas (doubling_ring, tripling_ring, quadrupling_ring) close the algebraic operations, and no_degree3_composition assembles them into the degree-exclusion statement.
why it matters in Recognition Science
The module supplies the positivity engine required by the DAlembert degree-exclusion results, which in turn feed the forcing-chain steps that establish J-uniqueness and the phi fixed point. It closes an algebraic gap that would otherwise allow nontrivial solutions in mismatch equations derived from the Recognition Composition Law.
scope and limits
- Does not treat complex or negative values of t.
- Does not prove the full DAlembert theorem, only the listed sibling lemmas.
- Does not connect the positivity result to the phi ladder or physical constants.
- Does not address compositions of degree higher than three.