NoDisjointDiameterEdges
plain-language theorem explainer
For all sufficiently large finite planar point sets, every pair of ordered edges realizing the diameter is geometrically non-disjoint: the two segments meet. This is the Hopf–Pannwitz geometric observation, packaged as an asymptotic predicate. Downstream proofs cite it as one thrackle-side hypothesis when bounding diameter-shell multiplicity. The declaration is a pure Prop abbreviation, not a proved statement.
Claim. The following asymptotic property holds: there exists $N$ such that for every $n \ge N$ and every finite set $A \subset \mathbb{R}^2$ with $|A|=n$, if $\Delta$ is a diameter distance of $A$ (every pairwise distance is at most $\Delta$, and $\Delta$ is attained), then no two ordered pairs realizing distance $\Delta$ determine geometrically disjoint segments in the plane.
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 a positive distance the ordered multiplicity is twice the unordered one, so classical bounds $\le n$ become $\le 2n$.
Points live in the Euclidean plane (Point2). A diameter shell for a finite set $A$ is a distance $\Delta$ that is attained and maximal among pairwise distances. The ordered diameter edges are the ordered pairs in $A$ at distance exactly $\Delta$. Two such edges are geometrically disjoint when the corresponding closed segments do not meet.
Classically, Hopf–Pannwitz observed that any two diameter segments of a finite planar set intersect. That four-point geometric fact is the intended content of this predicate; a sibling local-meeting hypothesis discharges it.
proof idea
There is no proof body: the declaration is a Prop definition, an asymptotic filter statement (∀ᶠ n in atTop) quantifying over finite planar sets of cardinality $n$, diameter shells $\Delta$, and pairs of ordered diameter edges, asserting they are never geometrically disjoint.
The intended discharge path is the one-line bridge no_disjoint_diameter_edges_from_local_meeting, which lifts a local lemma (any two diameter segments in the same finite planar set meet) through the filter. That local lemma is the four-point geometric core named in the module comment.
why it matters
This predicate is one of the two thrackle-side components of the Hopf–Pannwitz diameter bound in the RS treatment of Erdős #132. Combined with an ordered thrackle bound it yields the ordered diameter multiplicity bound and then diameter-shell sparsity (diameter_ordered_bound_from_thrackle_components, diameter_shell_sparse_from_thrackle_components).
Those sparsity facts feed the final assemblies erdos132_from_thrackle_and_no_deep_layer and related legacy undirected variants: diameter sparsity plus a no-deep-layer statement in the low-shell regime give the ordered Erdős #132 claim. In RS language, diameter-shell occupancy is a two-body recognition-energy count; controlling it is part of the distance-shell multiplicity program in this module.
The definition itself does not close the geometry: the local meeting lemma must still be supplied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.