Formalize the Casas–Alvero conjecture for prime-power degrees in Lean 4

Over a field $K$ of characteristic zero, with `P : K[X]` monic, prove (currently a `sorry` in google-deepmind/formal-conjectures): ``` theorem casas_alvero.prime_power (p k : ℕ) (hp : p.Prime) (hd : P.natDegree = p^k) (hP' : HasCasasAlveroProp P) : ∃ α : K, P = (X - C α) ^ P.natDegree ``` Meaning: if a monic $P\in K[X]$ has degree $p^k$ ($p$ prime) and the Casas–Alvero property (for each $1\le i<\deg P$, $P$ and its $i$-th derivative $P^{(i)}$ share a common root), then $P=(X-\alpha)^{\deg P}$ for some $\alpha\in K$.

Acceptance. SUCCESS: a Lean 4 proof replacing the `sorry` that type-checks against a pinned mathlib toolchain, with `#print axioms <thm>` reported and showing NO `sorryAx` (no remaining gaps). Expected pure-kernel: the only axioms should be `[propext, Classical.choice, Quot.sound]`; state explicitly that this holds. Also acceptable as separate milestones (distinct `sorry`s in the same file): the `double_prime_power` (degree $2p^k$) case. The positive-characteristic counterexample case already carries an external `formal_proof` link in the repo, so is NOT sought here.