feat(Archive): simplify Abel–Ruffini with certified root counting

[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 has 1,388 library lines in five modules:

• Sturm.Defs and Sturm.Basic develop generalized Sturm chains, sign variations, and interval and whole-line root counts. 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.
• RealRootCount.Parse and RealRootCount interpret the polynomial, request a candidate chain, and emit the checked proof.

The dependency set consists of six Mathlib-free Hex packages: HexRealRoots, HexPolyZ, HexPoly, HexModArith, HexArith, and HexBasic. All are declared directly using main, as required by Mathlib's CI revision policy, and lake-manifest.json pins exact published commits. The corresponding bridge development remains synchronized in hex-dev #10101; a script compares the five library modules and both test modules after namespace and module-path translation.

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 Hex pins are compatible with Mathlib's Landlock build. Starting without HexArith build artifacts, all Hex dependencies and native libraries were rebuilt with /tmp unwritable, followed by Mathlib, the archive module, and both regression modules. The C recipes keep compiler temporary files under .lake, and obsolete private bv_decide proofs that invoked an external temporary-file-using solver were removed.

🤖 Prepared with Codex

[github-actions]

PR summary 888804b26d

Import changes exceeding 2%

%	File
+2.72%	Mathlib.Tactic

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic	3015	3097	+82 (+2.72%)

Import changes for all files

Files	Import difference
Mathlib.Tactic	82
Mathlib.Tactic.RealRootCount.Parse (new file)	1121
Mathlib.Analysis.Polynomial.Sturm.Defs (new file)	1570
Mathlib.Analysis.Polynomial.Sturm.Basic (new file)	2070
Mathlib.Analysis.Polynomial.Sturm.Certificate (new file)	2396
Mathlib.Tactic.RealRootCount (new file)	2401

---

Declarations diff (regex)

+ 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
+ countSignChanges
+ countSignChanges_congr
+ countSignChanges_cons_cons
+ countSignChanges_nil
+ countSignChanges_singleton
+ 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
+ filter_ne_zero_congr
+ 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
+ signVariations_congr
+ signVariations_cons
+ signVariations_cons_ne
+ signVariations_cons_zero
+ signVariations_nil
+ signVariations_singleton
+ sign_changes_of_opposite
+ sign_mul_eq_neg_one
+ 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
+ variations
- 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 -- pending)

Computed after the build finishes.

---

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

Current commit 888804b26d
Reference commit 71a80585ee

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).