Hopf problem: threefold · special periods 4

Supporting definitions and proofs for this stage of the six-sphere construction.

theorem Mathoverflow1973.SpecialPeriods.TauCusp.exponential_norm_lt_one_of_upperHalfPlane {s : ℂ} (hs : 0 < s.im) : ‖CuspUniformization.exponential s‖ < 1