endpoint_disjoint_diameter_representatives_meet_simply_from_unique_live
plain-language theorem explainer
Given uniqueness of intersection points for endpoint-disjoint diameter edges, those edges meet simply: they share exactly one point. Discrete geometers working the RS form of Erdős #132 cite this to close the endpoint-disjoint half of the local diameter-representative theorem. The proof obtains existence from the four-point diameter crossing theorem, then feeds the uniqueness certificate.
Claim. If two distinct diameter-shell ordered edges on a finite point set $A\subset\mathbb{R}^2$ share no endpoint, and any common point of their closed segments is unique whenever it exists, then those edges meet simply: there is exactly one point lying on both closed segments.
background
The module physicalizes Erdős problem #132: a distance value is a shell in the pairwise Euclidean spectrum, read as a two-body recognition-energy shell whose multiplicity is shell occupancy. Ordered pairs are used for bookkeeping; for positive distances, ordered multiplicity is twice the unordered count, so classical $\le n$ becomes $\le 2n$.
A diameter shell is the unique maximal distance $\Delta$ realized by $A$. Diameter ordered edges are the ordered pairs at that distance. Two such edges meet simply when their closed segments intersect in exactly one point. The uniqueness certificate asserts only that endpoint-disjoint diameter representatives cannot share more than one point; existence of an intersection is already supplied by the four-point diameter crossing theorem.
The companion cross-distance bound records that every pairwise distance among the four endpoints is at most $\Delta$, which is the geometric input the crossing theorem needs.
proof idea
Term-mode proof. Unpack the two ordered edges as pairs $(a,b)$ and $(c,d)$. Apply the diameter cross-distance lemma to obtain all six pairwise distances $\le\Delta$. From the no-shared-endpoint hypothesis, extract the four inequalities $a\ne c$, $a\ne d$, $b\ne c$, $b\ne d$. Feed those inequalities and the six distance bounds into the four-point diameter crossing theorem to produce a geometric intersection point $x$. Uniqueness of any second candidate $y$ is exactly the uniqueness certificate applied to the same data, so the edges meet simply.
why it matters
This is the endpoint-disjoint half of the local diameter-representative geometry needed for the RS reading of Erdős #132. Downstream, the live Conway-form assembly theorem takes the uniqueness certificate as a hypothesis and routes through this implication (together with the already-proved shared-endpoint case and pointwise deep-layer screening) to obtain the ordered Erdős #132 statement. A second eventual assembly uses related diameter-sparsity machinery toward the same target.
In the module's language, diameter edges are the outermost two-body recognition shells. Simple meeting of endpoint-disjoint diameter representatives is the geometric control that keeps shell occupancy from exploding via thrackle-type crossings. The result does not itself invoke the forcing chain (T5–T8) or the RCL; it is pure plane geometry sitting under the combinatorial shell-count bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.