Erdős problem #1082

Resolve the first few-distance classification junction without open-ended search.

First action: Obtain Shinohara 2008, DOI 10.1016/j.disc.2007.08.028, or an author-hosted exact coordinate description; verify its uniqueness theorem and encode only the displayed 12-point set.

Stop or redirect when: Stop if primary coordinates or uniqueness cannot be sourced, the set does not have exactly five distances, or the theorem does not cover every 12-point five-distance set; otherwise record only the rigorously implied n <= 13 scope.

• Exact audit of Shinohara's unique 12-point five-distance extremizer.
  Encode the primary coordinates in triangular-lattice integer pairs and verify exactly five norms plus every determinant, with positive and negative controls.
• Focused search for later general-position isosceles-triangle bounds.
  Trace citations from Pach-Tardos and Nivasch et al.; translate every applicable bound through the explicit equal-radius-pair inequality before retaining it.
• Generic exact quadratic-field certificate checker.
  Parameterize the ring discriminant and JSON coordinates, then require a separate SymPy or Lean replay for any candidate.

• extremal incidence double counting
  Seek an upper bound for general-position isosceles triangles stronger than the two-apices-per-base count and translate it into a distance bound.
• exact finite classification transfer
  Combine published g(k) maxima and uniqueness results with exact determinant checks on every extremizer.
• counterexample and witness search
  Separate global and local distance counts, represent coordinates in Z[sqrt(3)], test every triple determinant and pairwise squared distance exactly, and use few-distance classifications only after checking collinearity.

• Freshly rebuild the historical H8 Lean proof during this epoch.
  Only 1.4 GB was free and the required Mathlib build cache was absent.
  Reopen only if: At least 6 GB verified free or a complete compatible shared .olean cache.
• Use unrestricted g(k) values without inspecting extremal configurations.
  Extremizers may contain collinear triples.
  Reopen only if: Primary exact coordinates, all-triples determinant check, and verified classification coverage.
• Transfer convex-position local improvements directly to arbitrary no-three-collinear sets.
  Their improvement uses strict convexity and cyclic order, neither implied by noncollinearity.
  Reopen only if: A proved replacement for the cap/good-edge lemmas using only NonTrilinear hypotheses.
• Use H8 as a global counterexample.
  It has four global distances, exactly floor(8/2).
  Reopen only if: None for H8 itself; a different exact configuration is required.