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

Draft

kim-em wants to merge 20 commits into

leanprover-community:masterfrom

kim-em:abel-ruffini-hex

Commits on Sep 15, 2026

feat(Analysis/Polynomial): certified real root isolation with Hex
kim-em
committed
8729c54
refactor: certify root counts from algebraic Sturm identities
kim-em
committed
53e0f11
refactor(Analysis/Polynomial): polish Sturm proofs and root counting
kim-em
committed
4359a98
fix: follow Mathlib's dependency revision policy
kim-em
committed
20e2138
test(RealRootCount): synchronize test source headers
kim-em
committed
58012b6
refactor(RealRootCount): simplify proofs and preserve elaboration context
kim-em
committed
8d14c35
fix(build): pin Hex releases compatible with Mathlib's sandbox
kim-em
committed
7afd880
fix(build): remove HexArith temporary-file dependency
kim-em
committed
b395520
refactor(Archive): certify the Abel-Ruffini root count
kim-em
committed
018bde5
build: use transitive Hex dependencies
kim-em
committed
eae2eb0
build: satisfy dependency revision policy
kim-em
committed
8db47d2
build: use the Hex v0.2.0 release
kim-em
committed
b75aa81
refactor(Sturm): use connectedness for constant signs
kim-em
committed
dbd6383
feat(Topology): constant signs on preconnected sets
kim-em
committed
3d28eab
refactor(Sturm): make firstSign total
kim-em
committed
d867f32
refactor(Tactic): share the Hex polynomial parser
kim-em
committed
2253a93
build: update Hex to v0.3.0
kim-em
committed
0ae7f2e
build: prepare Hex root-count dependencies
kim-em
committed
1a9606e
refactor(Sturm): use the shared List.signVariations API
kim-em
committed
237738a

Commits on Sep 16, 2026

Merge master into abel-ruffini-hex
kim-em
committed
73f9006