Claims

../

2014_06_08_sheffer: Sheffer's survey lists phi(n,4,3) = O(n/sqrt(log n)), the answer yes, from the triangular lattice, which contains two-distance rhombi; the bound is true by Grayzel's theorem, but this argument does not prove it.

2026_01_13_grayzel: For every n at least 2, n points of a box in the lattice (a, b root 2) have order n over root log n distances while every four determine at least three, so the answer is yes; confirmed by the site's curator, Lean assuming Bernays.

2026_01_29_feng: The Aletheia agent's proof: the n points of the ring of integers of Q(root -7) nearest the origin have order n over root log n distances and contain no square, equilateral triangle or pentagon trapezoid, so the answer is yes.

---