Hopf problem: threefold · special periods 2

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

theorem Mathoverflow1973.SpecialPeriods.CuspFamily.Data.iteratedCover_eq_iff (D : Data) (x y : ↥(CuspUniformization.LogCover D.radius)) : D.iteratedCover x = D.iteratedCover y ↔ CuspUniformization.TotalPeriodRelated D.correction ↑x ↑y