endpoint_disjoint_local_meeting_from_four_point
plain-language theorem explainer
Assuming the universal four-point diameter crossing lemma, any two endpoint-disjoint diameter segments in a finite planar point set eventually meet. Discrete-geometry and RS shell-multiplicity arguments cite this as the local geometric bridge from four-point geometry to the diameter-edge meeting property. The proof unpacks diameter-edge membership, reads off four endpoint inequalities, bounds the four cross-distances by the diameter shell, and applies the four-point hypothesis.
Claim. If every pair of endpoint-disjoint diameter segments in the plane whose six pairwise distances are at most the common length $\Delta$ have intersecting closed segments, then eventually (in $n$) the following holds: for every $n$-point planar set $A$ and every diameter shell value $\Delta$ of $A$, any two ordered diameter edges of $A$ that share no endpoint meet geometrically as closed segments.
background
This module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, and shell occupancy is multiplicity. Ordered pairs are used for Lean bookkeeping; for positive distances ordered multiplicity is twice the unordered count, so classical $\le n$ becomes $\le 2n$.
A diameter shell $\Delta$ is a value in the ordered pairwise distance spectrum of a finite set $A\subset\mathbb{R}^2$ that is maximal among those distances. Diameter ordered edges are the ordered pairs in $A\times A$ realizing distance exactly $\Delta$. Endpoint-sharing of two ordered edges is the disjunction of the four endpoint equalities; its negation is four strict inequalities.
The hypothesis is the $n$-free four-point core: any two endpoint-disjoint pairs of length $\Delta$ whose four cross-distances are $\le\Delta$ have intersecting closed segments (the Hopf–Pannwitz geometric nucleus). The target is the local meeting bridge: eventually in $n$, on any $n$-point set, endpoint-disjoint diameter edges meet.
proof idea
Tactic proof via filter_upwards on the atTop quantifier in the target. Fix $n$, an $n$-point set $A$, a diameter shell $\Delta$, and two diameter ordered edges $e,f$ that do not share an endpoint.
Unpack Finset filter/product membership to recover $e_1,e_2,f_1,f_2\in A$ and $\mathrm{dist}(e_1,e_2)=\mathrm{dist}(f_1,f_2)=\Delta$. From $\neg$ endpoint-sharing, obtain the four inequalities $e_i\ne f_j$.
Because $\Delta$ is a diameter shell, every spectrum value is $\le\Delta$. Every distinct pair from $A$ contributes its distance to the ordered spectrum, so the four cross-distances are $\le\Delta$. Feed the eight data (four inequalities, two equalities to $\Delta$, four cross bounds) into the four-point hypothesis to conclude the segments meet.
why it matters
This is the local geometric reduction step in the RS treatment of Erdős #132 (distance-shell multiplicity). It converts the universal four-point diameter crossing lemma into the endpoint-disjoint local meeting bridge used by diameter-edge arguments on finite planar sets.
Downstream, erdos132_from_four_point_thrackle_and_no_deep_layer assembles this bridge with a thrackle support bound and a no-deep-layer hypothesis toward the ordered Erdős #132 statement. That parent notes the four-point diameter geometry is live and proved, while the preferred counting input in the final endpoint is Conway rather than the deprecated undirected support bound.
In framework terms the result is pure planar discrete geometry feeding shell-occupancy control; it does not itself invoke the forcing chain (T5–T8), RCL, or the phi-ladder mass formula, but it underwrites the combinatorial side of recognition-energy shell multiplicity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.