sixUnorderedPairs
plain-language theorem explainer
The complete set of six unordered pairs among four labeled plane points. Combinatorialists and discrete geometers cite it as the ambient container for any edge support on a four-point set. The body is a literal six-element Finset of Sym2 pairs, not a derived construction.
Claim. For four points $a,b,c,d$ in the Euclidean plane, define the finite set of unordered pairs $\{\{a,b\},\{a,c\},\{a,d\},\{b,c\},\{b,d\},\{c,d\}\}$.
background
The module Distance Shell Multiplicity records the Recognition Science reading of Erdős problem #132: a distance value is a two-body recognition-energy shell, and its multiplicity is shell occupancy. Ordered pairs are used for Lean convenience; for positive distances, ordered multiplicity is twice the unordered count, so classical bounds $\le n$ become $\le 2n$.
Point2 is the Euclidean plane $\mathbb{R}^2$. Unordered pairs are elements of $\mathrm{Sym}_2(\mathrm{Point2})$, so each edge is independent of endpoint order. On a four-point ambient set the complete unordered graph $K_4$ has exactly $\binom{4}{2}=6$ edges; this definition names that six-element container explicitly.
Downstream bookkeeping treats any edge support whose endpoints lie in ${a,b,c,d}$ as a subset of this fixed six-pair set, which is the pigeonhole container used in the Conway–thrackle $K_4$ arguments.
proof idea
Pure definition: the right-hand side is the literal Finset whose six members are $\mathrm{Sym}_2$ of the ordered pairs $(a,b)$, $(a,c)$, $(a,d)$, $(b,c)$, $(b,d)$, $(c,d)$. No lemmas are applied; cardinality and subset facts are proved separately.
why it matters
This is the standard pigeonhole container for unordered edge supports on four ambient points. It feeds six_unordered_pairs_card_eq_six (cardinality equals 6 under distinctness) and unorderedEdgeSupport_subset_sixUnorderedPairs_of_card_eq_four (any edge set on a four-point ambient set sits inside this Finset).
Those two facts unlock the conditional and unconditional noncollinear Conway-conditioned $K_4$ support bounds: under a Conway thrackle hypothesis and not-all-collinear, the unordered support has size at most 4. In the RS framing this is discrete geometry supporting distance-shell multiplicity control for Erdős #132, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.