support_edges_meet_simply_symm
plain-language theorem explainer
The support-level simple-meeting relation on unordered planar edges is symmetric: if two support edges meet simply relative to an ordered edge set, they meet simply when the pair is swapped. Cite this when working with ordered orientations of undirected edges in the Erdős #132 distance-shell physicalization. The proof unpacks the two ordered witnesses, swaps them, and applies ordered simple-meeting symmetry.
Claim. Let $E$ be a finite set of ordered pairs of points in the Euclidean plane, and let $u,v$ be unordered edges (elements of $\mathrm{Sym}_2$ of the plane). If $u$ and $v$ meet simply at the support level with respect to $E$ (i.e., they admit ordered representatives in $E$ whose closed segments share exactly one point), then $v$ and $u$ also meet simply at the support level with respect to $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. Ordered pairs are used 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$.
Points live in the Euclidean plane $\mathbb{R}^2$. Support-level simple meeting means two unordered support edges $u,v$ have ordered representatives $e,f\in E$ whose unordered projections recover $u$ and $v$, and whose closed segments share exactly one point. That formulation is the right one for ordered edge sets that contain both orientations of the same undirected edge.
The immediate upstream fact is the ordered-level symmetry: if two ordered edges meet simply, so do the swapped pair.
proof idea
Short term-mode argument by witness swap. Destructure the hypothesis into ordered edges $e,f\in E$, the two unordered-projection equalities, and the ordered simple-meeting fact. Rebuild the existential for the reversed pair by exchanging $e$ with $f$ (and swapping the membership and projection hypotheses). Discharge the remaining ordered simple-meeting goal by applying the ordered symmetry lemma ordered_edges_meet_simply_symm.
why it matters
In the RS reading of Erdős #132, simple meetings of support edges control how planar distance shells interact geometrically. Symmetry of the support-level relation is pure bookkeeping: unordered edge geometry must not depend on the order in which the two support classes are named. No downstream consumers are recorded yet; the lemma is local infrastructure inside DistanceShellMultiplicity, sitting beside diameter-shell uniqueness, sparse-shell divergence, and the ordered spectrum/multiplicity apparatus. It does not touch the forcing chain (T0–T8), the Recognition Composition Law, or the phi-ladder mass formula; it only stabilizes the combinatorial geometry layer that feeds shell-occupancy counting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.