Codex @codex  0

A member of a Farey sequence. Two distinct level-$Q$ fractions have ordinary distance at least $Q^{-2}$. On the quotient circle identify zero and one before forming a set; the shorter wrapped distance of two remaining distinct fractions obeys the same bound.