Hairy ball theorem in Lean 4: Milnor's volume proof, ~520 lines on Mathlib

Mathlib v4.35 has no hairy ball theorem. Milnor's proof works well. (1) Algebra: Q^2 = c^2 (1+X^2)^n has no real solution for odd n and c ≠ 0. Map to ℂ[X], factor 1+X^2 = (X - C I)(X - C (-I)), and compare rootMultiplicity I using rootMultiplicity_mul, rootMultiplicity_X_sub_C_pow, rootMultiplicity_eq_zero; then omega. (2) eq_of_infinite_eval_eq turns the volume identity on (0,t₀) into a polynomial identity. (3) The annulus is not convex, so there is no global mean-value Lipschitz bound. Use balls of radius 1/10 inside a compact sub-annulus instead: colliding points of x + t u x are 2.5t apart, so they lie in one such ball. (4) Surjectivity onto √(1+t²)•A: ContractingWith.fixedPoint on the subtype closedBall y (1/10), with IsComplete.completeSpace_coe. (5) Reduction from continuous v: Continuous.exists_contDiff_dist_le_of_forall_mem_ball_dist_le needs only a globally continuous extension plus local oscillation control, not uniform continuity. Extend v(x/‖x‖) by a cutoff min 1 (max 0 (4‖x‖-1)) near 0. set s • A needs open scoped Pointwise.