theorem Polynomial.trailingCoeff_eraseLead {P : Polynomial ℝ} (h : P.eraseLead ≠ 0) : P.eraseLead.trailingCoeff = P.trailingCoeff

eraseLead only removes the top coefficient, so it leaves the trailing coefficient unchanged (as long as it does not empty the polynomial).

theorem Polynomial.countP_pos_modTwo_monic {n : ℕ} {Q : Polynomial ℝ} (hQ : Q.IsMonicOfDegree n) : Multiset.countP (fun (x : ℝ) => 0 < x) Q.roots ≡ if SignType.sign Q.trailingCoeff = 1 then 0 else 1 [MOD 2]

Core (monic case): the number of positive roots of a monic real polynomial is congruent modulo two to the indicator of its trailing coefficient's sign.

theorem Polynomial.countP_pos_modTwo {P : Polynomial ℝ} (hP : P ≠ 0) : Multiset.countP (fun (x : ℝ) => 0 < x) P.roots ≡ if SignType.sign P.leadingCoeff = SignType.sign P.trailingCoeff then 0 else 1 [MOD 2]

The number of positive roots of a nonzero real polynomial is congruent modulo two to the end-sign indicator [sign leadingCoeff ≠ sign trailingCoeff].

theorem Polynomial.signVariations_modTwo {P : Polynomial ℝ} (hP : P ≠ 0) : P.signVariations ≡ if SignType.sign P.leadingCoeff = SignType.sign P.trailingCoeff then 0 else 1 [MOD 2]

The number of sign variations of a nonzero real polynomial is congruent modulo two to the end-sign indicator [sign leadingCoeff ≠ sign trailingCoeff].

theorem Polynomial.signVariations_parity (P : Polynomial ℝ) (hP : P ≠ 0) : Multiset.countP (fun (x : ℝ) => 0 < x) P.roots ≡ P.signVariations [MOD 2]

Descartes parity. For a nonzero real polynomial the number of positive roots (with multiplicity) and the number of sign variations of the coefficients have the same parity.

theorem Polynomial.countP_pos_eq_zero_of_signVariations_eq_zero {P : Polynomial ℝ} (h : P.signVariations = 0) : Multiset.countP (fun (x : ℝ) => 0 < x) P.roots = 0

No sign variations forces no positive roots.

theorem Polynomial.countP_pos_eq_one_of_signVariations_eq_one {P : Polynomial ℝ} (hP : P ≠ 0) (h : P.signVariations = 1) : Multiset.countP (fun (x : ℝ) => 0 < x) P.roots = 1

Exactly one sign variation forces exactly one positive root.