Counting real roots of a concrete ℚ-polynomial in Lean/Mathlib (for Galois group = S_p arguments)

Mathlib's Polynomial.Gal.galActionHom_bijective_of_prime_degree' needs Fintype.card (p.rootSet ℝ) + 1 ≤ Fintype.card (p.rootSet ℂ) ≤ Fintype.card (p.rootSet ℝ) + 3. The complex count is easy (card_rootSet_eq_natDegree irreducible.separable (IsAlgClosed.splits _)). The real count is the hard part; the Archive quintic does it with Rolle + IVT, which does not scale to e.g. a septic with 5 real roots.

What worked: a Sturm-sequence certificate over List ℤ checked by decide +kernel (the checker only multiplies/adds integer polynomials; the certificate generator can even be run inside the decide since kernel evaluation of pseudo-division at degree 7 is fast). Bridge from rootSet to roots.toFinset:

have hset : p.rootSet ℝ = ↑((q : ℝ[X]).roots.toFinset) := by rw [rootSet_def, aroots, hp]  -- hp : p.map (algebraMap ℚ ℝ) = q
rw [← Nat.card_eq_fintype_card, hset, Nat.card_coe_set_eq, Set.ncard_coe_finset]

rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe] fails with 'motive is not type correct' because the Fintype instance depends on the set; going through Nat.card avoids it.

Other gotchas from the same proof: galActionHom lives in Polynomial.Gal (open it); the Fact (map (algebraMap ℚ ℂ) p).Splits instance must be enabled with attribute [local instance] splits_ℚ_ℂ; compute_degree! / monicity! handle natDegree/Monic of the explicit polynomial; Eisenstein via IsPrimitive.Int.irreducible_iff_irreducible_map_cast + irreducible_of_eisenstein_criterion with interval_cases n <;> simp [p, coeff_X_pow] for the coefficient conditions. Result: X^7 - 10X^5 + 10X^3 + 2 not solvable by radicals, ~100 lines.