Erdos132Ordered
plain-language theorem explainer
Ordered-pair form of Erdős #132: every sufficiently large finite planar point set carries at least two distinct sparse Euclidean distance shells. Discrete geometers and RS shell-flux arguments cite this Prop as the formal target. It is a pure definition (filter-eventually over cardinality), not a proved theorem; residual packages elsewhere discharge it.
Claim. For all sufficiently large $n\in\mathbb{N}$, every finite $A\subset\mathbb{R}^2$ with $|A|=n$ admits distinct $r,s\in\mathbb{R}$ such that both the $r$-shell and the $s$-shell of $A$ are sparse (ordered-pair multiplicity at most $2n$).
background
This module physicalizes Erdős problem #132 inside Recognition Science. Classically a distance value is a shell in the pairwise Euclidean spectrum; physically it is a two-body recognition-energy shell whose occupancy is the multiplicity. The ambient space is the Euclidean plane (Point2 as $\mathbb{R}^2$).
Lean works with ordered non-diagonal pairs. For any positive distance the ordered multiplicity is exactly twice the unordered one, so the classical sparsity threshold $\le n$ becomes $\le 2n$. A shell at radius $r$ is sparse when that ordered occupancy bound holds.
The statement is phrased with the filter atTop on $\mathbb{N}$: the property is required only for all large enough cardinalities, matching the classical "sufficiently large finite set" wording of #132.
proof idea
No proof body: this is a Prop abbreviation. It packages the filter-quantified claim
$\forall^\infty n,;\forall A\subset\mathbb{R}^2,;|A|=n\Rightarrow\exists r\neq s$ both sparse shells.
Downstream theorems instantiate this type by feeding residual hypotheses (Conway thrackle bounds, deep-layer screening, endpoint-disjoint uniqueness, etc.) into wrapper lemmas that construct the two radii.
why it matters
This is the canonical RS target for Erdős #132 in ordered-pair normalization. Dozens of residual packages land here: Conway-counting plus deep-screening, endpoint-disjoint collinearity or uniqueness packs, constructive and large-nonstar current residuals, diameter-sparsity plus no-deep-layer, and thrackle variants. Each erdos132_from_* theorem has type ending at this Prop, so closing any residual package proves the ordered #132 statement.
In the RS reading, sparse shells are low-occupancy two-body recognition-energy levels; multiplicity control is shell-flux bookkeeping. A stronger sibling target asks that the number of sparse shells diverge. The definition itself does not invoke the forcing chain (T5–T8) or the mass ladder; it is pure discrete geometry sitting under the RS physicalization layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.