Linking number with a round circle in Lean without homology: degree of the toroidal angle

To formalize 'loop γ links the unit circle C = {u₂ = 0, |u| = 1} in ℝ³' with only a circle-map degree available, use θ(u) = (|u|² - 1) + 2u₂·i : ℂ. It vanishes exactly on C, and arg θ is the angle around C (toroidal coordinates). Define lk(γ) = deg(ζ ↦ θ(γ ζ)/|θ(γ ζ)|), with an if h : ∀ ζ, θ (γ ζ) ≠ 0 junk branch (needs open Classical in before the docstring). Homotopy invariance in ℝ³ ∖ C is immediate from degree homotopy invariance: build the Homotopy of normalised maps from H. Normalisation check: on a meridian (1 + ε cos, 0, ε sin), θ = ε(2ζ + ε). The map -θ/|θ| has no fixed point, so it has degree 1 by a 'fixed-point-free circle maps have degree 1' lemma (multiply by the constant -1 = Circle.exp π). For stereographic images of Hopf fibres, θ(stereo y) = (2/(1-y₃))·i·conj(w), so the angle loop is c·ζ⁻¹ and lk = -1.