feat: certified root counting via Hex, and simplify Abel-Ruffini

[kim-em]

The Abel–Ruffini archive proof previously spent most of its problem-specific argument bounding the real roots of X ^ 5 - 4 * X + 2: it differentiated twice for the upper bound, then used continuity and explicit sign estimates for the lower bound. This replaces that development with a certified Sturm computation:

theorem not_solvable_by_rad' (x : ℂ) (hx : aeval x (Φ ℚ 4 2) = 0) :
    x ∉ solvableByRad ℚ ℂ := by
  apply not_solvable_by_rad 4 2 2 x hx (by real_root_count) <;> decide

The archive file shrinks from 175 to 127 lines and no longer imports Analysis.Calculus.LocalExtr.Polynomial. Its reusable Galois-theoretic helper now takes the mathematically relevant premise that the polynomial has exactly three real roots; Hex discharges that premise for the concrete witness. The final Abel–Ruffini theorem and witness are unchanged.

real_root_count proves the number of distinct real roots of a closed, squarefree polynomial over ℚ with integer coefficients and positive degree. Hex supplies an untrusted candidate signed remainder chain. The elaborator clears denominators and emits ordinary Mathlib polynomials; ring, compute_degree, and norm_num verify the recurrence identities, positive factors, derivative relation, separability, and variation count. No correctness theorem for Hex's representation or generator is trusted.

The supporting Mathlib development adds 1,303 library lines across seven modules:

• ContinuousOn.sign and IsPreconnected.sign_eq_of_continuousOn provide the general topology fact that a continuous nonvanishing function has constant sign on a preconnected set.
• Sturm.Defs and Sturm.Basic develop generalized Sturm chains and interval and whole-line root counts using List.signVariations from [Merged by Bors] - feat(Data/List/SignVariations): add List.signVariations #43783. These modules are independent of Hex.
• Sturm.Certificate turns positive scaled remainder identities into a checked chain, proves separability, and derives a root-set cardinality.
• HexPolyZ.Parse and RealRootCount interpret the polynomial, request a candidate chain, and emit the checked proof.

The only direct dependency is the Mathlib-free HexRealRoots package at the coordinated Hex v0.5.0 release. Although its package manifest pins the wider release closure, the modules used here import only the pure Lean HexRealRoots, HexPolyZ, HexPoly, and HexBasic roots. hex-dev #10131 removed an umbrella import that had unnecessarily exposed the native NTT implementation. The original bridge source was synchronized in the merged hex-dev #10125. This PR now uses the upstream List.signVariations API throughout: the Sturm definitions and sign-congruence arguments, the tactic’s integer-side count, and the generated proofs via the public recursion lemma. The duplicate local counters and congruence proofs have been removed. hex-dev #10273 bumps the source monorepo to the matching Mathlib revision and synchronizes all seven shared library/test modules with this version.

Tests cover endpoint conventions, constant chains, local let expressions, negative leading coefficients, nontrivial content, and larger coefficients. Diagnostic tests reject zero, constants, repeated roots, noninteger coefficients, free variables, unsupported goals, and incorrect requested counts. The Sturm theorem, certificate cardinality lemma, and final Abel–Ruffini theorems use only propext, Classical.choice, and Quot.sound.

The usual clean-checkout cache invariant is preserved:

lake clean
lake exe cache get
lake build --no-build

The final command succeeds without compiling anything. Mathlib's portable cache keeps its existing package set and key space; while building the cache executable, Lake compiles the exact transitive closure of the three external modules imported here, then cache get restores the Mathlib artifacts. From empty Hex build directories this compiled 19 pure Lean modules in 14 seconds: one from HexBasic, fifteen from HexPoly, one from HexPolyZ, and two from HexRealRoots. Neither HexArith nor HexModArith module libraries entered the build. Keeping these modules outside the portable cache also keeps the trusted master cache writer and the PR cache reader on identical keys in fork CI.

🤖 Prepared with Codex

[github-actions]

PR summary 73f9006e5a

Import changes exceeding 2%

%	File
+2.83%	Mathlib.Tactic

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic	3038	3124	+86 (+2.83%)

Import changes for all files

Files	Import difference
Mathlib.Tactic	86
Mathlib.Topology.Instances.Sign.Connected (new file)	874
Mathlib.Tactic.HexPolyZ.Parse (new file)	1120
Mathlib.Analysis.Polynomial.Sturm.Defs (new file)	1570
Mathlib.Analysis.Polynomial.Sturm.Basic (new file)	2075
Mathlib.Analysis.Polynomial.Sturm.Certificate (new file)	2404
Mathlib.Tactic.RealRootCount (new file)	2409

---

Declarations diff (regex)

+ ContinuousOn.sign
+ IsPreconnected.sign_eq_of_continuousOn
+ IsSturmChain
+ IsSturmChain.sturm
+ IsSturmChain.sturm_Ioc
+ RemainderChain
+ RemainderChain.card_rootSet
+ RemainderChain.cons
+ RemainderChain.isSturmChain
+ RemainderChain.pair
+ RemainderChain.separable
+ RemainderIdentity
+ SignRelation
+ SignRelation.signVariations_eq
+ card_filter_Ioc_split
+ chainZeros
+ constantChain
+ coprime_of_remainder
+ emit
+ eval_ne_zero_of_isCoprime
+ eval_sign_eq_of_no_zero
+ eval_sign_neg_inf
+ eval_sign_pos_inf
+ exists_left_gap
+ exists_right_gap
+ firstSign
+ firstSign_cons_ne
+ firstSign_cons_zero
+ firstSign_nil
+ head_mem
+ intTerm
+ linearChain
+ mem_chainZeros
+ mul_sign_near_root
+ ne_zero
+ nestedPolynomial
+ nonempty
+ polyTerm
+ remainderIdentity
+ signRelation_eval
+ signVariations_cons
+ sign_changes_of_opposite
+ sign_near_root
+ sturmVar
+ sturmVarNegInf
+ sturmVarPosInf
+ sturmVar_cons_zero
+ sturmVar_const_of_no_zero
+ sturmVar_eq_right
+ sturmVar_interior_cross
+ sturmVar_nil
+ sturmVar_root_cross
+ testPolynomial
- real_roots_Phi_ge
- real_roots_Phi_ge_aux
- real_roots_Phi_le

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 73f9006).

• +56 new declarations
• −0 removed declarations

+ContinuousOn.sign
+IsPreconnected.sign_eq_of_continuousOn
+Mathlib.Tactic.HexPolyZ.Parse.evalCoeff
+Mathlib.Tactic.HexPolyZ.Parse.evalIntCoeff
+Mathlib.Tactic.HexPolyZ.Parse.evalRat
+Mathlib.Tactic.HexPolyZ.Parse.getNat
+Mathlib.Tactic.HexPolyZ.Parse.parsePoly
+Mathlib.Tactic.RealRootCount.tacticReal_root_count
+Mathlib.Tactic.RealRootCount.termReal_root_count_
+Sturm.IsSturmChain
+Sturm.IsSturmChain.casesOn
+Sturm.IsSturmChain.head
+Sturm.IsSturmChain.head_mem
+Sturm.IsSturmChain.interior_alternates
+Sturm.IsSturmChain.last_no_root
+Sturm.IsSturmChain.mk
+Sturm.IsSturmChain.ne_zero
+Sturm.IsSturmChain.nonempty
+Sturm.IsSturmChain.nonzero_mem
+Sturm.IsSturmChain.rec
+Sturm.IsSturmChain.recOn
+Sturm.IsSturmChain.root_flank
+Sturm.IsSturmChain.sturm
+Sturm.IsSturmChain.sturm_Ioc
+Sturm.RemainderChain
+Sturm.RemainderChain.card_rootSet
+Sturm.RemainderChain.casesOn
+Sturm.RemainderChain.cons
+Sturm.RemainderChain.coprime
+Sturm.RemainderChain.interior_alternates
+Sturm.RemainderChain.isSturmChain
+Sturm.RemainderChain.last_no_root
+Sturm.RemainderChain.mk
+Sturm.RemainderChain.nonzero_mem
+Sturm.RemainderChain.pair
+Sturm.RemainderChain.rec
+Sturm.RemainderChain.recOn
+Sturm.RemainderChain.separable
+Sturm.chainZeros
+Sturm.eval_sign_neg_inf
+Sturm.eval_sign_pos_inf
+Sturm.firstSign
+Sturm.firstSign_cons_ne
+Sturm.firstSign_cons_zero
+Sturm.firstSign_nil
+Sturm.mem_chainZeros
+Sturm.signVariations_cons
+Sturm.sturmVar
+Sturm.sturmVarNegInf
+Sturm.sturmVarPosInf
+Sturm.sturmVar_cons_zero
+Sturm.sturmVar_const_of_no_zero
+Sturm.sturmVar_eq_right
+Sturm.sturmVar_interior_cross
+Sturm.sturmVar_nil
+Sturm.sturmVar_root_cross

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 73f9006e5a
Reference commit fcabd43b03

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.