Erdős 1041: add a quantitative unit-disc root-retention variant

[wcook04]

Closes #5048.

1041.lean asks for a path of length less than 2 inside {z | ‖f(z)‖ < 1} joining two roots of a monic polynomial whose roots lie in the unit disc. This PR does not answer that.

It adds one formally proved neighbouring lemma:

theorem erdos_1041.variants.perturbed_roots_in_unit_disk
    (f : Polynomial ℂ) (hf : f.Monic) (hdeg : 0 < f.natDegree)
    (hsplit : f.Splits) {ρ ε : ℝ} (hρ : 0 ≤ ρ)
    (hroots : ∀ b ∈ f.roots, ‖b‖ ≤ ρ) (hε : 0 < ε)
    (hmargin : ((f.natDegree + 1) * ε) ^ (f.natDegree : ℝ)⁻¹ + ρ < 1)
    {shift : ℂ} (hshift : ‖shift‖ < ε) :
    ∀ a : ℂ, (f + Polynomial.C shift).eval a = 0 → ‖a‖ < 1

If every root of f already lies in a disc of radius ρ < 1, a sufficiently small constant perturbation keeps every root inside the open unit disc. The margin is explicit. The lemma is placed in a second namespace Erdos1041 block so it does not inherit the open conjecture's bundled hypotheses.

Proof:
https://github.com/wcook04/plectis-lean-erdos249-257/blob/f88e8b686908010a43e9078dda49abbabcfc4079/adapters/FormalConjecturesVariants.lean#L178-L186

Repository: https://github.com/wcook04/plectis-lean-erdos249-257

No new FormalConjecturesForMathlib file is needed. The statement uses only Mathlib polynomial vocabulary already imported by the problem file. The linked adapter theorem is proposition-identical.

This does not produce a short path in the lemniscate and does not settle erdos_1041. No originality or priority claim is made for perturbation of polynomial roots.

AI Usage Disclosure: the linked Lean development and this contribution were produced with AI assistance. I have reviewed the statement identity, the linked proof, and this diff, and I take responsibility for the submission.

Note

This records a solved quantitative variant adjacent to Erdős 1041. The path-length conjecture remains open.