shared_endpoint_diameter_representatives_meet_simply
plain-language theorem explainer
Distinct unordered diameter edges that share an endpoint meet simply: their four endpoints form a noncrossing configuration under the diameter shell constraints. Anyone assembling the diameter-support Conway condition for the ordered Erdős #132 statement cites this. The proof cases on the four shared-endpoint patterns and reduces each, via distance commutativity and unordered-edge swaps, to the shared-left representative lemma.
Claim. For every finite point set $A \subset \mathbb{R}^2$ and every diameter shell value $\Delta$ on $A$, if $e$ and $f$ are ordered diameter edges realizing $\Delta$, their underlying unordered edges are distinct, and $e,f$ share an endpoint, then $e$ and $f$ meet simply (the two edges form a noncrossing simple junction at the shared vertex).
background
The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, and shell multiplicity is occupancy. Ordered pairs are used for bookkeeping; for positive distances, ordered multiplicity is twice the unordered count, so the classical bound $\le n$ becomes $\le 2n$.
A diameter shell on a finite set $A$ is a distance value $\Delta$ equal to the diameter of $A$. Diameter ordered edges are the ordered pairs in $A\times A$ realizing that distance. Two ordered edges share an endpoint when one of the four endpoint-equalities holds; they meet simply when the geometric junction at a shared vertex is noncrossing (no thrackle-type double cover of the same unordered support).
The predicate discharged here is the endpoint-sharing half of the local diameter-representative theorem: whenever two distinct unordered diameter support edges share a vertex, their ordered lifts meet simply. The companion half (endpoint-disjoint representatives) is handled elsewhere via four-point diameter crossing.
proof idea
Tactic proof by exhaustive case analysis. Introduce the set $A$, diameter $\Delta$, the diameter-shell hypothesis, and two ordered diameter edges $e,f$ that are unordered-distinct and share an endpoint. Destructure $e=(a,b)$ and $f=(c,d)$.
Apply diameter_ordered_edges_cross_distances_le to obtain the six pairwise distance inequalities among ${a,b,c,d}$ (each pair distance $\le\Delta$, with the two diameter edges equal to $\Delta$). Unfold the shared-endpoint disjunction into four branches: $a=c$, $a=d$, $b=c$, $b=d$.
- Shared left endpoint ($a=c$): direct appeal to
shared_left_diameter_representatives_meet_simply. - Shared $a=d$: rebuild an unordered-distinctness hypothesis after swapping the second edge, apply the shared-left lemma with
dist_comm, then transport simplicity byordered_edges_meet_simply_swap_right. - Shared $b=c$: symmetric left-swap of the first edge, then
ordered_edges_meet_simply_swap_left. - Shared $b=d$: both edges swapped to a common left vertex, then both simplicity-swap lemmas.
All branches close by the shared-left core lemma plus edge-orientation transport.
why it matters
This theorem closes the shared-endpoint half of the diameter-support Conway condition in the ordered Erdős #132 pipeline. Downstream, erdos132_from_support_conway_endpoint_disjoint_uniqueness_and_deep_screening_live explicitly treats this case as already proved and only needs support-level Conway counting, endpoint-disjoint uniqueness, and deep-layer screening to finish the ordered statement.
It also feeds endpoint_disjoint_diameter_representatives_meet_simply_from_unique_live (the complementary meeting-simply route) and the eventual assembly erdos132_from_ordered_conway_and_eventual_no_deep_layer_live. In the module's RS reading, diameter shells are the extremal two-body recognition-energy shells; simple meeting of shared-endpoint diameter representatives is the local geometric control that keeps shell occupancy from thrackling, which is what forces the sparse-shell bound underlying Erdős #132.
No forcing-chain landmark (T5–T8) is directly invoked; the result is pure plane geometry in service of the multiplicity bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.