chosenSupportRepresentative_injective
plain-language theorem explainer
On a finite set of ordered planar pairs, the map that picks one ordered representative from each unordered support class is injective. Anyone counting shell supports via image cardinality needs this. The proof recovers the unordered edge from each representative and concludes the underlying classes coincide.
Claim. Let $E$ be a finite set of ordered pairs of points in $\mathbb{R}^2$. The map sending each unordered support class of $E$ to its chosen ordered representative is injective: distinct unordered classes receive distinct ordered pairs.
background
This module physicalizes Erdős problem #132 inside Recognition Science: a classical distance shell becomes a two-body recognition-energy shell, and shell multiplicity is occupancy. The development works with ordered pairs for Lean convenience; for positive distances the ordered multiplicity is exactly twice the unordered one, so classical bounds $\le n$ become $\le 2n$.
Here $E$ is a finite set of ordered pairs of planar points (Point2 is Euclidean $\mathbb{R}^2$). The unordered support of $E$ quotients each ordered edge to an unordered edge class. The chosen-support-representative map selects, for each such class that meets $E$, a single ordered pair in $E$. A companion fact states that forgetting order on the chosen representative recovers the original unordered class.
Injectivity of that choice map is the set-theoretic prerequisite for counting the chosen ordered support by image cardinality rather than by a separate enumeration.
proof idea
Tactic proof on two support-class elements $u,v$ with equal chosen representatives. Apply subtype extensionality, so it suffices to equate the underlying unordered edges $u.1$ and $v.1$. The companion lemma chosenSupportRepresentative_unordered says that unordered-of-ordered of the chosen representative of $u$ is $u.1$ (and likewise for $v$). A three-line calc chains $u.1$ to the unordered image of the common representative and then to $v.1$.
why it matters
Feeds directly into chosenOrderedSupport_card, which proves that the finset of chosen ordered representatives has the same cardinality as the unordered edge support, via Finset.card_image_of_injective. That equality is the bookkeeping step that lets ordered-pair formalization talk about unordered shell support sizes without double-counting artifacts.
In the broader Distance Shell Multiplicity development this keeps the RS reading of Erdős #132 honest: recognition-energy shells are tracked with ordered events, yet occupancy comparisons against classical unordered thresholds remain faithful. It is pure finite-set infrastructure, not a forcing-chain step (T0–T8), but it underwrites the multiplicity comparisons the module uses for sparse shells and diameter shells.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.