unorderedEdgeSupport_chosenOrderedSupport

This module physicalizes Erdős problem #132 inside Recognition Science: a classical distance value is a shell in the pairwise Euclidean spectrum; physically it is a two-body recognition-energy shell whose occupancy is the shell multiplicity. The development works with ordered pairs for Lean convenience. For any positive distance, ordered multiplicity is exactly twice the usual unordered multiplicity, so classical thresholds of the form $\le n$ become $\le 2n$.

Points are Point2, an abbreviation for the Euclidean plane $\mathbb{R}^2$. An ordered edge set is a finite set of pairs $(p,q)$. Its unordered edge support is the image under the forgetful map to unordered pairs (symmetric 2-sets), discarding orientation and collapsing $(p,q)$ with $(q,p)$. The chosen ordered support selects, for each unordered support class, a single ordered representative. The present identity says that selection does not change the unordered support.

Classical reasoning, then ext on unordered pairs $u$, proving both inclusions of Finset equality.

Left-to-right: if $u$ lies in the unordered support of the chosen system, unpack a witnessing ordered edge $e$ via the membership characterization of unordered support; the subset lemma for the choice map puts $e$ back in the original $E$, so $u$ is in the original unordered support.

Right-to-left: given $u$ in the original unordered support, package it as an attached subtype element, take the chosen support representative of that class, and verify two facts: the representative lands in the image that defines the chosen ordered support, and the representative maps back to the same unordered class $u$.

The sole downstream consumer is the transfer theorem that turns a standard ordered Conway thrackle support bound into a support-level bound: choose one ordered representative per unordered support edge, apply the ordered theorem to that chosen system, then push the cardinality bound back to unordered support. That transfer needs exactly this identity so that the chosen system and the original set share the same unordered support (hence the same support cardinality).

In the broader RS reading of Erdős #132, shell occupancy and support size control recognition-energy bookkeeping on planar point sets. The lemma is pure combinatorial hygiene inside that pipeline: it licenses moving between ordered bookkeeping (Lean-friendly) and unordered geometric support (the classical statement) without changing the support that thrackle-type inequalities constrain. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it sits in the mathematical substrate those physical claims later use.