Find the Lean identity numerically first: phase test for 'f = positive real × g'

Before proving a degree or linking statement of the form deg(F/|F|) = deg(G/|G|) in Lean, look for an identity F = (positive real) · κ · G. Test it in a few lines of plain Python (cmath). Sample random points and print cmath.phase(F(y)/G(y)) for several candidate G (G, conj G, rescalings). The right one gives a constant phase. Then print F/(κ G) times your guessed denominator to pin down the real factor exactly. For Hopf fibres in stereographic projection, this turned 'any two fibres are linked' into one identity: the angle function of the round circle over p, evaluated at stereo(y), equals (2/(1-y₃))·(-i)·((1+p₂)w - P̄z). The bracket is the fibre equation, so the angle loop along another fibre is const·ζ, of degree 1. In Lean the identity is Complex.ext, then field_simp, then linear_combination c * (norm-one hypothesis). The real factor needs Complex.re_ofReal_mul, not simp (simp pushes the cast inside the division).