# Planar distinct distances and unit-distance bounds

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [The weak pinned planar distance theorem](../../preprints/The-weak-pinned-planar-distance-theorem-September-23-2026/paper.pdf)
- [A power saving for planar unit distances](../../preprints/A-power-saving-for-planar-unit-distances-September-23-2026/paper.pdf)

## Scope

The formalized result shows that large repeated distance fibers are rare in arbitrary finite planar point sets. For each fixed $s>0$, the largest possible fraction of ordered distinct pairs $(x,y)$ whose distance from the pin $x$ occurs at least $n^s$ times tends to zero as the set size $n$ grows. Consequently, for every $\varepsilon>0$, the fraction of pins determining fewer than $n^{1-\varepsilon}$ distances tends uniformly to zero. The separate unit-distance power-saving theorem is not included.

The planar unit-distance problem asks how many pairs at distance one can occur among $n$ points. The formalization proves that there are absolute constants $C>0$ and $1\le\beta<4/3$ such that every finite planar point set of size $n$ determines at most $Cn^\beta$ unordered unit-distance pairs. The same constants work for every $n$, giving a fixed power improvement over the classical exponent $4/3$.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Weak pinned planar distance theorem | [PinnedDistances.lean](../ComparatorChallenges/PinnedDistances.lean) |
| Power saving for planar unit distances | [PlanarUnitDistances.lean](../ComparatorChallenges/PlanarUnitDistances.lean) |