unorderedEdgeSupport
plain-language theorem explainer
Maps a finite set of ordered planar point-pairs to the undirected edges obtained by forgetting orientation. Shell-multiplicity and Conway residual arguments cite this support when they need undirected cardinality rather than ordered pair counts. The body is a one-line Finset image under the ordered-to-Sym2 map.
Claim. Given a finite set $E$ of ordered pairs of points in the Euclidean plane $\mathbb{R}^2$, the unordered edge support is the finite set $\{\{p,q\}:(p,q)\in E\}\subseteq \mathrm{Sym}_2(\mathbb{R}^2)$ of undirected edges obtained by forgetting orientation.
background
The module physicalizes Erdős problem #132: a distance value is a two-body recognition-energy shell, and its multiplicity is shell occupancy. Lean works with ordered pairs; for positive distances the ordered multiplicity is twice the classical unordered count, so the classical threshold $\le n$ becomes $\le 2n$.
Points are planar: Point2 is the Euclidean plane $\mathbb{R}^2$. An ordered edge is a pair $(p,q)\in\mathbb{R}^2\times\mathbb{R}^2$. The sibling map that forgets orientation sends $(p,q)$ to the unordered pair ${p,q}$ in $\mathrm{Sym}_2(\mathbb{R}^2)$ (doc: "Forget orientation of an ordered edge").
This definition packages that map as a Finset image, producing the undirected support of any ordered edge set used later in diameter-shell and sparse-shell counting.
proof idea
One-line definition under classical choice: the support is the image of $E$ under the orientation-forgetting map $(p,q)\mapsto{p,q}$. No further lemmas are applied at the definition site; membership and cardinality properties are proved downstream from the image construction.
why it matters
Undirected support is the bridge from ordered pair bookkeeping to classical edge counts in the Erdős #132 physicalization. Downstream, a chosen ordered representative is selected for each support edge, and that chosen set has the same cardinality as the support. The support also feeds Conway residual bounds and the counting helper that if a support sits inside a six-edge ambient set missing two distinct edges then its size is at most four.
In the RS reading, shell occupancy is recognition-energy multiplicity on planar two-body events; collapsing orientation is the step that recovers the usual geometric edge set before multiplicity and sparseness statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.