Hopf problem: period family · core 5

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

theorem Mathoverflow1973.PeriodFamily.Boundary.Cusp.sin_two_pi_lt_neg_half (t : ℝ) (ht0 : -(3 / 8) < t) (ht1 : t < -(1 / 8)) : Real.sin (2 * Real.pi * t) < -(1 / 2)