chosenOrderedSupport_card
plain-language theorem explainer
For any finite set of ordered planar point pairs, the chosen-orientation representative finset has the same cardinality as the unordered edge support. Cite this when equating ordered and unordered edge counts in the Erdős #132 shell-multiplicity formalization (diameter shells, Conway thrackle bookkeeping). The proof is a short image-cardinality argument from injectivity of the representative map.
Claim. For every finite set $E$ of ordered pairs of planar points, the cardinality of the chosen-representative support of $E$ equals the cardinality of the unordered edge support of $E$.
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. The development uses ordered pairs 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 $E$ is a finite set of ordered pairs of planar points (Point2). The unordered edge support forgets orientation; the chosen ordered support keeps exactly one ordered representative per undirected edge. Equality of those two cardinalities is the bookkeeping fact needed before comparing shell counts to thrackle or diameter constraints.
proof idea
Work classically. Unfold the definition of the chosen ordered support, which is the image of the unordered support under a representative map. Rewrite the goal with Finset.card_image_of_injective: cardinality of an image equals the domain cardinality once the map is injective. The remaining injectivity obligation is discharged by the existing lemma that the chosen-support representative is injective on $E$; a short simp closes the residual identity.
why it matters
In the Erdős #132 RS physicalization, diameter edge sets and Conway-type thrackle conditions are stated most cleanly on unordered supports, while the Lean development prefers ordered pairs. This lemma licenses free passage between those two cardinalities, so shell-occupancy and diameter-shell uniqueness arguments do not double-count orientations.
The immediately following material notes that the Conway condition belongs on the unordered support precisely because diameter ordered edge sets contain both orientations and therefore cannot be Conway thrackles as ordered finsets. No downstream used_by edges are recorded yet; the result is local infrastructure for ordered-shell multiplicity, sparse shells, and the ordered Erdős #132 statements in this module rather than a named forcing-chain landmark (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.