chosenSupportRepresentative_unordered
plain-language theorem explainer
For any ordered edge set E of planar points, the canonically chosen ordered pair for an unordered support edge u recovers exactly that same unordered class. Anyone counting shell multiplicities or thrackle supports via ordered pairs needs this identity. The proof is a one-line extraction of the second component of Classical.choose_spec from the membership characterization of unordered support.
Claim. Let $E$ be a finite set of ordered pairs of points in $\mathbb{R}^2$, and let $u$ be an unordered edge (an element of $\mathrm{Sym}_2(\mathbb{R}^2)$) that lies in the unordered support of $E$. If $e$ is the canonically chosen ordered representative of $u$ in $E$, then the unordered edge associated to $e$ equals $u$.
background
The module Distance Shell Multiplicity records the Recognition Science physicalization of Erdős problem #132: classical distance shells become two-body recognition-energy shells, and shell multiplicity is occupancy. Ordered pairs are used for Lean simplicity; for positive distances, ordered multiplicity is twice the unordered count, so the classical bound $\le n$ becomes $\le 2n$.
Points are Point2, i.e. Euclidean space $\mathbb{R}^2$. An ordered edge set $E$ is a finite set of pairs. The unordered support collects the $\mathrm{Sym}_2$ classes of those pairs. Membership in that support is characterized by existence of an ordered representative: $u$ is in the support iff there exists $e\in E$ with unordered image equal to $u$.
The chosen support representative picks, via classical choice, one such ordered pair for each support class. This lemma states that the choice is faithful to the class it was chosen for.
proof idea
One-line term proof. Apply mem_unorderedEdgeSupport_iff to the subtype membership hypothesis $u.2$, obtaining existence of an ordered $e\in E$ with unordered image $u.1$. The definition of the chosen representative is exactly Classical.choose of that existence witness. Project the second component of Classical.choose_spec to conclude that the unordered image of the chosen pair equals $u.1$.
why it matters
This is the basic correctness identity for the choice map from unordered support classes to ordered pairs. Downstream it feeds three results in the same module: injectivity of the choice map (distinct support classes get distinct ordered representatives), equality of unordered supports between the original edge set and the chosen ordered support, and promotion of the support-level Conway thrackle condition to the ordinary ordered Conway condition on the chosen representative finset.
In the Erdős #132 physicalization, ordered bookkeeping must not invent or lose distance shells. Faithful recovery of the unordered class is the first step that lets thrackle and multiplicity arguments pass between ordered and unordered presentations without changing shell occupancy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.