rd-quartics-thm7prime: an unconditional, machine-verified repair of the classification of rational-derived quartics with a repeated root

First public release. Lean 4 formalization of Theorem 7′, the unconditional repair of the Buchholz–MacDougall (2000) classification of rational-derived quartics with a repeated root. Main statement: Thm7Statement.thm7prime (Thm7Prime/Master.lean, MD5 a1b1d54566481b50bd0ce3667c2ee509) Axiom footprint: [propext, Classical.choice, Quot.sound] — no custom axiom, no sorry Toolchain: leanprover/lean4:v4.31.0-rc1, mathlib d568c8c Reproduction: lake exe cache get && lake build (~30 min); the build log prints the per-declaration axiom report Includes: blueprint (natural-language ↔ Lean correspondence), Sage/Magma verification scripts, Gröbner certificates, session archive Companion note artifacts: https://doi.org/10.5281/zenodo.21465598