DiameterSegmentsMeetLocally
plain-language theorem explainer
Names the asymptotic local geometric property that any two diameter segments of a large finite planar point set meet. Anyone assembling the Hopf–Pannwitz diameter-edge bound or the ordered Erdős #132 bridge cites it. It is a pure Prop definition (filter-at-top over n-point sets), discharged later from the endpoint-disjoint core plus shared-endpoint cases.
Claim. The property that, for all sufficiently large $n$, every finite planar $n$-point set $A$ and every diameter value $\Delta$ of $A$, any two ordered edges of $A$ of length $\Delta$ meet geometrically as segments in the plane.
background
The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, with ordered-pair multiplicity exactly twice the unordered count (so the classical $\le n$ threshold becomes $\le 2n$). Points live in the Euclidean plane (Point2).
A diameter shell is the (unique) maximal pairwise distance realized by $A$. The ordered diameter edges are the ordered pairs at that distance. Geometric meeting means the corresponding closed segments intersect in the plane; geometric disjointness is the negation used by the sibling no-disjoint-diameter-edges property (the Hopf–Pannwitz observation).
This definition packages the full local meeting statement, including pairs that already share an endpoint. A companion core isolates the harder endpoint-disjoint case.
proof idea
No proof: the declaration is a bare Prop definition. It asserts, eventually for all large $n$, that every $n$-point planar set, every diameter shell $\Delta$, and every pair of ordered diameter edges, the two edges meet geometrically. Downstream lemmas discharge it by cases (shared endpoint versus endpoint-disjoint core).
why it matters
This is the four-point geometric core behind the no-disjoint-diameter-edges bridge and the Hopf–Pannwitz input to the ordered Erdős #132 assembly. Downstream, no_disjoint_diameter_edges_from_local_meeting turns meeting into absence of geometrically disjoint diameter edges; diameter_segments_meet_from_endpoint_disjoint_core builds the full meeting property from the endpoint-disjoint core plus the elementary shared-endpoint lemma; and the legacy erdos132_from_local_diameter_meeting_thrackle_and_no_deep_layer feeds meeting into the thrackle-support plus no-deep-layer route to the ordered Erdős bound. In the RS reading, diameter shells are the highest two-body recognition-energy shells, so controlling their local geometry controls shell occupancy at the top of the spectrum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.