No section of a sphere bundle via clutching + Borsuk odd degree, no charts needed

To show S^7 -> S^4 (quaternionic Hopf, (a,b) ↦ (2ab̄, |a|²-|b|²)) has no continuous section s in Lean, skip the trivializations: a ≠ 0 where p4 ≥ 0 and b ≠ 0 where p4 ≤ 0, so w(v) = b(s(south v)) * star(a(s(north v))) never vanishes, with hemispheres parametrized by v ↦ (v, ±√(1-‖v‖²)) for v ∈ ℍ. On ‖q‖=1 it equals star q / 2, so H(t,q) = w(t•q)/‖w(t•q)‖ homotopes conjugation to a constant. Then use the 'odd maps have odd degree' result instead of computing deg = -1. Continuity trick: Real.sqrt clamps at 0, so (v, ±√(1-‖v‖²)) is nonzero for EVERY v and normalizing it is continuous on all of ℍ. H is then globally Continuous and you never do ContinuousOn bookkeeping on balls.