orderedShellMultiplicity_pos_of_mem
plain-language theorem explainer
Membership of a real value in the ordered pairwise distance spectrum of a finite planar point set forces strictly positive ordered shell occupancy at that value. Anyone working the ordered-pair form of Erdős #132, or its RS reading as two-body recognition-energy shells, cites this positivity fact. The argument is a short classical unpacking: spectrum membership supplies a witnessing ordered pair, so the filtered cardinality is positive.
Claim. Let $A$ be a finite set of points in the Euclidean plane and let $r\in\mathbb{R}$. If $r$ lies in the ordered pairwise distance spectrum of $A$, then the ordered shell multiplicity of $A$ at $r$ is strictly positive.
background
This module records the Recognition Science physicalization of Erdős problem #132. Classically a distance value is a shell in the set of pairwise Euclidean distances; physically it is a two-body recognition-energy shell, and its multiplicity is the shell occupancy. The development uses ordered pairs for Lean simplicity: for a positive distance, ordered multiplicity is exactly twice the usual unordered multiplicity, so the classical threshold $\le n$ becomes $\le 2n$.
Points are elements of the Euclidean plane $\mathbb{R}^2$. The ordered distance spectrum of a finite set $A$ is the image of the non-diagonal ordered pairs under Euclidean distance. Ordered shell multiplicity at radius $r$ is the cardinality of the set of ordered pairs in $A$ that realize distance $r$. The claim is the elementary occupancy sanity check: spectrum membership means at least one such pair exists.
proof idea
Classical reasoning is enabled so Finset image and card lemmas apply. Both the spectrum and the multiplicity definitions are unfolded. Membership of $r$ in the spectrum is rewritten via Finset.mem_image, producing a witnessing ordered pair $pq$ together with the equality that its distance equals $r$. Positivity of the multiplicity then follows from Finset.card_pos by exhibiting that same pair inside the filtered set of pairs at distance $r$ (discharged by simp on the membership and equality hypotheses).
why it matters
The lemma is local bookkeeping infrastructure for the ordered-pair formulation of distance-shell multiplicity. It underwrites later notions in the same module (sparse shells, diameter shells, and the supercritical regime for occupied non-sparse shells flagged by the next doc-comment). In the RS reading, a realized two-body recognition-energy shell cannot carry zero ordered occupancy once it appears in the spectrum.
No downstream consumers are currently attached in the dependency graph, so the result does not yet feed a named parent theorem or a forcing-chain landmark (T0–T8). Its role is to keep the Erdős #132 physicalization free of empty-shell edge cases when occupancy arguments begin.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.