chosenOrderedSupport
plain-language theorem explainer
For a finite ordered edge set in the plane, pick exactly one ordered pair per unordered support edge. Anyone transferring Conway thrackle bounds from ordered pairs to unordered support cardinality cites this selector. The construction is the image of the attached unordered support under a fixed representative map.
Claim. Given a finite set $E$ of ordered pairs of points in $\mathbb{R}^2$, form the finite set of ordered pairs obtained by choosing, for each unordered support edge of $E$, one ordered representative via a fixed choice map on that support.
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 Euclidean points (Point2 as $\mathbb{R}^2$). An ordered edge set $E$ is a finite set of ordered pairs. Its unordered support collapses each pair ${p,q}$ regardless of order. The sibling choice map chosenSupportRepresentative picks one ordered orientation per such unordered edge; the present definition packages those choices into a single finset.
Upstream geometry supplies the planar point type and edge-set conventions used throughout the bipartite distance spectrum development.
proof idea
Definitional, not a proof. Under classical choice, take the unordered support of $E$, attach elementhood proofs, and image under the fixed representative map that sends each unordered support edge to one ordered pair. The result is a finset of ordered pairs with one representative per support edge.
why it matters
This selector is the bridge from unordered support language to ordinary ordered Conway thrackle statements. Downstream, the chosen set is a subset of $E$, has the same cardinality as the unordered support, and has the same unordered support as $E$. The support-level Conway condition promotes to the ordered Conway condition on the chosen set, which lets the standard ordered thrackle bound transfer back to a support-cardinality bound (conway_support_bound_on_support_from_ordered).
In the RS reading of Erdős #132, shell occupancy bounds control how many ordered pair events can share a recognition-energy distance. The thrackle route is one combinatorial path toward those multiplicity controls inside the distance-shell program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.