card_le_four_of_two_missing
plain-language theorem explainer
If a finite set S of unordered planar pairs sits inside a six-element set T and misses two distinct members of T, then |S| ≤ 4. Used as a pure counting step inside the conditional Conway thrackle K4 support bound for distance-shell multiplicity. The argument is elementary Finset arithmetic: S is contained in the four-element difference T minus those two pairs.
Claim. Let $S \subseteq T$ be finite sets of unordered pairs of planar points, with $|T| = 6$. If two distinct elements $m_1, m_2 \in T$ both lie outside $S$, then $|S| \le 4$.
background
The ambient module physicalizes Erdős problem #132: a Euclidean distance value is a shell of pairwise distances, read in RS as a two-body recognition-energy shell whose multiplicity is shell occupancy. Ordered pairs are used for Lean convenience; for positive distances the ordered multiplicity is twice the unordered one, so classical thresholds scale by two.
Here the carrier is Point2 (planar points from the bipartite distance spectrum), and the objects are finite sets of unordered pairs Sym2 Point2, i.e. undirected edges. The six-element ambient set $T$ is the combinatorial type of the complete edge set on four distinct points ($\binom{4}{2} = 6$). The lemma is a pure cardinality helper: once two distinct edges of that complete set are known to be absent from a subset $S$, the subset cannot exceed four elements.
proof idea
Classical Finset reasoning, no geometry. First show $S \subseteq T \setminus {m_1,m_2}$ from $S \subseteq T$ and the two non-membership hypotheses (case-split on membership in the two-element insert). The pair set ${m_1,m_2}$ has cardinality 2 by distinctness, and sits inside $T$ by the membership hypotheses. Then Finset.card_sdiff_of_subset with $|T|=6$ yields $|T \setminus {m_1,m_2}| = 4$. Conclude by Finset.card_le_card on the inclusion of $S$ into that difference.
why it matters
Feeds the conditional four-point Conway thrackle support bound in the same module: under a Conway thrackle hypothesis on an ordered edge set $E$, not-all-collinear, and the assumption that the unordered edge support sits inside the standard six-pair Finset on four ambient points, one obtains $|\mathrm{unorderedEdgeSupport}, E| \le 4$.
The conditional shape deliberately splits the long subset-inclusion casework from the dichotomy-plus-Conway argument; this counting lemma discharges the final cardinality step once two edges are known missing. The unconditional K4 bound then follows by enumerating the inclusion when the ambient point set has cardinality 4. In the broader RS reading, that bound constrains shell occupancy for four-point configurations in the Erdős #132 physicalization (distance shells as recognition-energy shells).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.