EndpointDisjointDiameterSegmentsMeetLocally
plain-language theorem explainer
Names the residual local geometric core for Erdős #132 in the plane: for all large n, any two diameter edges of an n-point set that share no endpoint must meet as segments. Cited by the full diameter-meeting bridge and the ordered Erdős-132 assembly. Pure Prop definition (eventually-for-all packaging); no proof obligation here.
Claim. For all sufficiently large $n$, every finite $A\subset\mathbb{R}^2$ with $|A|=n$, and every diameter-shell value $\Delta$ of $A$, if $e,f$ are ordered diameter edges of $A$ at distance $\Delta$ that do not share an endpoint, then the corresponding segments meet geometrically.
background
The module physicalizes Erdős problem #132: a classical distance value is a shell in the pairwise Euclidean spectrum; in RS it is a two-body recognition-energy shell whose occupancy is the multiplicity. Ordered pairs are used for Lean simplicity, so classical multiplicity $\le n$ becomes ordered multiplicity $\le 2n$.
Points live in Point2 (Euclidean plane $\mathbb{R}^2$). A diameter shell is a distance value $\Delta$ realized as the maximum pairwise distance of a finite set $A$. The ordered diameter-edge set collects ordered pairs from $A$ at exact distance $\Delta$. Endpoint-sharing of two such ordered edges is the elementary case; geometric meeting means the underlying undirected segments intersect in the plane.
This Prop isolates what remains after endpoint-sharing is discharged: endpoint-disjoint diameter segments must cross or touch.
proof idea
Definition only: a Prop abbreviation packing an ∀ᶠ n in atTop statement. No tactics, no lemmas applied. Downstream, the four-point diameter-crossing lemma discharges it by reducing endpoint-disjoint pairs to four distinct points whose cross-distances are at most the diameter; the shared-endpoint case is handled separately by an elementary lemma.
why it matters
This is the geometric bottleneck of the RS treatment of Erdős #132. The theorem diameter_segments_meet_from_endpoint_disjoint_core lifts it, together with the shared-endpoint lemma, to the full local meeting bridge DiameterSegmentsMeetLocally. Separately, endpoint_disjoint_local_meeting_from_four_point shows the four-point crossing lemma implies this core. The legacy assembly erdos132_from_endpoint_disjoint_diameter_core_thrackle_and_no_deep_layer feeds the core plus thrackle-support and no-deep-layer hypotheses into the ordered Erdős-132 statement. In the module's language, diameter shells are the extremal two-body recognition-energy shells; controlling their local incidence geometry is what forces the multiplicity bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.