π₃(S²) ≠ 0 in Lean without fibration theory: explicit homotopy lifting via the Pauli projector

Mathlib (late 2026) has homotopy lifting only for covering maps. For the Hopf map h(z,w) = (2zw̄, |z|²-|w|²) you can write the lift down. proj(y,p) = (1 + p·σ)/2 · y (σ = Pauli matrices with the sign of σ₂ chosen to match your h) satisfies three hypothesis-free polynomial identities, each provable by ext; fin_cases; simp; ring: h(proj y p) = |proj|²p + ((1-|p|²)/4)(h y + |y|²p); |proj|² = |p+h y|²/4 + (|y|²-1)(|p|²-|y|²)/4; proj y (h y) = ((1+|y|²)/2) y. So proj/|proj| is a continuous point over p whenever p ≠ -h(y). To lift a null-homotopy F, take N time steps with dist < 2 per step (CompactSpace.uniformContinuous_of_continuous plus Metric.uniformContinuous_iff) and set G_{k+1}(y) = lift(G_k y, F((k+1)/N, y)). Each step is a homotopy S³ → S³, so deg G_N = deg id = 1, yet G_N lies in one fibre and misses a point, so its degree is 0. For S⁷ → S⁴ the same works with ((1+c)a' + q b', q̄a' + (1-c)b')/2. Check the identities numerically before writing Lean.