chosenSupportRepresentative_mem
plain-language theorem explainer
For a finite set of ordered planar point-pairs, any chosen ordered representative of an unordered support class lies in the original set. Used when converting between ordered edge sets and their Sym2 support in the distance-shell multiplicity development. Proof is a one-line Classical.choose_spec extraction after the unordered-support membership iff.
Claim. Let $E$ be a finite set of ordered pairs of points in $\mathbb{R}^2$. If $u$ is an unordered pair in the unordered edge support of $E$, then the chosen ordered representative of $u$ (relative to $E$) is an element of $E$.
background
The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, with multiplicity as shell occupancy. Points are planar Euclidean points (Point2 as $\mathbb{R}^2$). Edges are stored as ordered pairs for Lean convenience; for positive distances, ordered multiplicity is twice the unordered count, so classical thresholds $\le n$ become $\le 2n$.
Unordered edge support collects the Sym2-classes of pairs that appear (in either order) in a finite ordered edge set $E$. A chosen support representative picks, for each such class, a concrete ordered pair witnessing membership. The characterizing lemma equates membership of an unordered pair in that support with existence of an ordered pair in $E$ whose Sym2 class matches.
proof idea
Term-mode one-liner. From the subtype hypothesis that $u$ lies in the unordered edge support of $E$, apply the membership characterization (mem_unorderedEdgeSupport_iff) to obtain an existence statement. Classical.choose_spec on that witness yields a pair in $E$ together with the Sym2 identification; project to the first component to conclude the chosen representative is in $E$.
why it matters
Local hygiene lemma for the ordered/unordered bridge in the distance-shell multiplicity stack. It is the membership half needed by chosenOrderedSupport_subset, whose doc-comment states that chosen support representatives are drawn from the original ordered edge set; that subset fact keeps subsequent shell-occupancy and sparse-shell arguments inside the original Finset rather than an ambient product space.
In the broader RS reading, shells are recognition-energy levels on planar two-body configurations. Keeping representatives inside $E$ ensures multiplicity counts and diameter-shell uniqueness stay tied to the physical edge set, not to an abstract Sym2 quotient. No forcing-chain landmark (T5–T8) is touched directly; the lemma is pure combinatorial support for the Erdős #132 physicalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.