chosenOrderedSupport_subset
plain-language theorem explainer
Chosen ordered support representatives of a finite set of ordered planar pairs all lie inside the original set. Anyone transferring Conway thrackle bounds from ordered edges to unordered support cites this inclusion. The argument is a short term proof: unfold the image definition and apply the representative-membership lemma.
Claim. For any finite set $E$ of ordered pairs of points in the Euclidean plane $\mathbb{R}^2$, the set of chosen ordered support representatives of $E$ is contained in $E$.
background
This module physicalizes Erdős problem #132 inside Recognition Science: classical distance shells become two-body recognition-energy shells, and shell multiplicity is occupancy. Ordered pairs are used for Lean bookkeeping; for a positive distance, ordered multiplicity is twice the unordered count, so classical thresholds scale by two.
Points are planar Euclidean points (Point2). An ordered edge set $E$ is a finite set of ordered pairs. The chosen ordered support of $E$ selects, for each unordered support edge, one ordered representative via a representative map. The companion fact that each such representative lands in $E$ is the membership lemma used here.
The local goal is to pass between ordered edge systems and their unordered supports cleanly, so thrackle-type cardinality bounds can be stated at support level without double-counting artifacts.
proof idea
Term-mode proof under classical logic. Fix an element $e$ of the chosen ordered support. Unfold that support as the image of the representative map, rewrite membership via Finset.mem_image, and unpack a preimage unordered edge $u$ with $e$ equal to the chosen representative of $u$. Conclude by the already-proved fact that every chosen support representative of an unordered edge from $E$ lies in $E$.
why it matters
The inclusion is the first half of the ordered-to-unordered support bridge. Downstream, it feeds the equality that the chosen representative set has exactly the same unordered support as the original ordered edge set. That equality, together with this subset, lets the standard ordered Conway thrackle bound transfer to a support-level form: pick one ordered representative per unordered support edge, apply the ordered theorem to the chosen system, then push the cardinality bound back to the support.
In the RS reading of Erdős #132, shell occupancy and thrackle-type geometric constraints control how many two-body recognition-energy shells a planar configuration can carry. This lemma is pure bookkeeping, but without it the Conway support bound on support cannot be stated from the ordered hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.