Integer parabola points have pairwise distinct distances
ProvedEsgk.parabola_sqDist_injdiscrete-geometrydistinct-distances
For and in , if then and . Hence distinct nonnegative integer points have pairwise distinct distances: an -point set of this form is in general position and determines exactly distances. Supporting construction fact for exact distinct-distance bounds; proves no lower bound by itself.
Preamble
import Mathlib
Formal statement
namespace Esgk
theorem parabola_sqDist_inj {a b c d : ℕ} (hab : b < a) (hcd : d < c) : (a - b) ^ 2 * (1 + (a + b) ^ 2) = (c - d) ^ 2 * (1 + (c + d) ^ 2) → a = c ∧ b = d := by sorry
end EsgkSource
Integer parabola squared-distance injectivity; Lean source artifact: esgk-on3 lean/Esgk/Parabola.lean (Esgk.parabola_sqDist_inj), kernel-checked 2026-09-16; skeptic audit artifact: docs/skeptic-parabola-sqdist-2026-09-16.md.