shared_left_diameter_representatives_meet_simply
plain-language theorem explainer
Distinct diameter segments that share a common left endpoint in the plane meet at exactly that endpoint. Anyone proving the diameter-support Conway condition for Erdős #132 shell multiplicity cites this. The proof shows any second intersection forces collinearity and equal right endpoints, contradicting distinct unordered edges.
Claim. Let $a,b,c\in\mathbb{R}^2$ and $\Delta\in\mathbb{R}$. If the unordered edges $\{a,b\}$ and $\{a,c\}$ are distinct, $\mathrm{dist}(a,b)=\mathrm{dist}(a,c)=\Delta$, and $\mathrm{dist}(b,c)\le\Delta$, then the closed segments $[a,b]$ and $[a,c]$ share exactly one point.
background
The module physicalizes 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 simplicity; for positive distances, ordered multiplicity is twice the unordered count, so classical thresholds double.
Points live in the Euclidean plane (Point2). Two ordered edges meet simply when their closed segments share exactly one point; this is the meeting condition in the Conway straight-line thrackle theorem, which excludes overlapping collinear segments that would inflate pairwise-meeting counts past $|A|$.
Upstream segment facts used here: the left endpoint always lies on its closed segment, and a point on $[a,b]$ at distance $\mathrm{dist}(a,b)$ from $a$ must be $b$. Orientation vanishing on segments and a lens-collinearity criterion place a third point on a diameter segment when distances and planarity align.
proof idea
First rule out $a=b$: that would force $\Delta=0$, hence $c=a$, collapsing the two unordered edges. Positivity of $\Delta$ follows. The unique-meeting witness is $a$, which lies on both closed segments by the left-endpoint lemma.
Uniqueness is by contradiction. Any other common point $y$ forces $\mathrm{orient}_2(a,b,y)=\mathrm{orient}_2(a,c,y)=0$, hence (after swaps) $\mathrm{orient}_2(a,y,b)=\mathrm{orient}_2(a,y,c)=0$. Transitivity of orientation zero yields $\mathrm{orient}_2(a,b,c)=0$. The lens criterion then puts $c$ on $[a,b]$. Equal left-endpoint distances force $c=b$, contradicting distinct unordered edges.
why it matters
This is the left-endpoint half of the shared-endpoint diameter lemma. Downstream, shared_endpoint_diameter_representatives_meet_simply packages left and right cases to discharge the endpoint-sharing half of the diameter-support Conway condition: distinct unordered diameter support edges that share an endpoint meet simply.
In the Erdős #132 physicalization, diameter shells are the extremal two-body recognition-energy shells. Simple meeting keeps thrackle-style edge counts honest, so shell multiplicity cannot be inflated by collinear overlaps. The result is pure planar geometry feeding the sparse-shell and flux-bridge siblings in the same module; it does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law, but it underwrites the combinatorial side of the RS reading of distance shells.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.