Repeated-distance four-sets and isosceles triples

../

_proof: Count extensions of equal-side triples and separate equal-length pairs by their number of distinct endpoints.

---

The proof is a complete author-recorded counting argument by Plasma AI. No independent review or Lean proof is recorded. Its inequality uses no external distance theorem.

Together with the external bound $Q(P)=O(n^3\log n)$, it makes the $n^{3+o(1)}$ question in Problem 1087 equivalent to a uniform bound $I(P)\le n^{2+o(1)}$. The research account states that source premise and its reading limit. No gap remains in these inequalities; the near-quadratic isosceles estimate is still an additional obligation. Verification is direct double counting.