Small-factor extraction for reducible polynomials

A reducible polynomial of degree n always has an irreducible factor of degree at most n / 2: it splits as a product of two non-units whose degrees sum to n, and the smaller of the two dominates an irreducible factor.

This is the pigeonhole step of Rabin's irreducibility test (see CompPoly/Data/Polynomial/Rabin.lean), which needs to bound the degree of a hypothetical small factor in order to derive a contradiction.

Main statements

• Polynomial.exists_factor_natDegree_le_of_reducible: a reducible polynomial of degree n has an irreducible factor of degree at most n / 2.

theorem Polynomial.exists_factor_natDegree_le_of_reducible {R : Type u_1} [Field R] (P : Polynomial R) {n : ℕ} (h_deg : P.natDegree = n) (h_pos : 0 < n) (h_red : ¬Irreducible P) : ∃ (q : Polynomial R), Irreducible q ∧ q ∣ P ∧ q.natDegree ≤ n / 2

A reducible polynomial of positive degree n has an irreducible factor of degree at most n / 2.

Writing P = a * b with both factors non-units, their degrees sum to n, so the smaller one has degree at most n / 2; any irreducible factor of it works.