chosenSupportRepresentative
plain-language theorem explainer
Given a finite set of ordered planar pairs and one unordered edge in its support, this definition selects a single ordered representative of that edge. Anyone promoting support-level thrackle or shell-occupancy arguments to ordered edge finsets will cite it. The body is a one-line classical choice from the membership characterization of the unordered support.
Claim. For a finite set $E$ of ordered pairs of points in $\mathbb{R}^2$ and an unordered edge $u$ in the unordered support of $E$, there is a chosen ordered pair $(p,q)\in E$ whose unordered class equals $u$.
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. Ordered pairs are used 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$.
Here Point2 is the Euclidean plane $\mathbb{R}^2$. The unordered edge support of an ordered edge finset $E$ is the set of $\mathrm{Sym}_2$ classes of pairs that appear in $E$. The upstream membership lemma states that $u$ lies in that support if and only if there exists an ordered $e\in E$ with the same unordered class.
proof idea
One-line noncomputable definition. Apply the membership characterization of the unordered support to the subtype proof that $u$ is supported, obtaining an existential witness $\exists e\in E$ with matching unordered class; then take Classical.choose of that witness. Noncomputability is solely from classical choice.
why it matters
This selector is the atom under the chosen ordered support: the image of the attached unordered support under the map yields one ordered representative per support edge. Downstream facts record that the representative lies in the original ordered set, recovers the correct unordered class, is injective on support classes, and that the chosen finset has exactly the same unordered support as $E$. The support-level Conway thrackle condition then promotes to the ordinary ordered Conway condition on the chosen finset. Together these steps let shell-occupancy and thrackle arguments in the Erdős #132 physicalization move cleanly between unordered support geometry and ordered pair events.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.