no_disjoint_diameter_edges_from_local_meeting
plain-language theorem explainer
Local meeting of diameter segments on finite planar point sets implies that the diameter-edge graph eventually has no geometrically disjoint pair. Anyone assembling the ordered Erdős #132 bound from the Hopf–Pannwitz geometry cites this bridge. The proof is a one-line filter-upwards reduction: meeting immediately negates disjointness.
Claim. Assume that, for all sufficiently large $n$, every $n$-point planar set $A$ and every diameter value $\Delta$ of $A$ has the property that any two ordered diameter edges of $A$ at length $\Delta$ meet geometrically. Then, for all sufficiently large $n$, no two ordered diameter edges of such an $A$ at length $\Delta$ are geometrically disjoint.
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 Lean bookkeeping, so the classical multiplicity threshold $\le n$ becomes $\le 2n$.
A diameter shell is a distance value $\Delta$ realizing the maximum pairwise distance in a finite planar set $A\subset\mathbb{R}^2$. The local meeting hypothesis asserts that, eventually in $n$, any two ordered diameter edges of $A$ at that $\Delta$ intersect geometrically (the four-point core behind Hopf–Pannwitz). The target property is the dual phrasing: eventually no two such edges are geometrically disjoint.
Both statements are formulated as eventualities along atTop in $n$, quantified over finite point sets of cardinality $n$ and over diameter shells of those sets.
proof idea
Term-mode one-liner. Apply filter_upwards to the local-meeting hypothesis so the same large-$n$ tail is used. On that tail, fix $A$, a diameter shell $\Delta$, and two ordered diameter edges $e,f$. The meeting hypothesis supplies geometric intersection of $e$ and $f$. The assumed geometric disjointness of $e$ and $f$ is then contradicted by that intersection, which is exactly the negation required by the no-disjoint-diameter-edges property.
why it matters
This is the pure logical bridge from the four-point diameter-meeting geometry to the no-disjoint-diameter-edge formulation used in thrackle-style counting. Downstream it is fed into erdos132_from_local_diameter_meeting_thrackle_and_no_deep_layer, the legacy assembly of the ordered Erdős #132 statement from local diameter meeting, an undirected thrackle support bound, and a no-deep-layer hypothesis in the low-shell regime.
In the Recognition Science reading, diameter shells are the extremal two-body recognition-energy shells; ruling out disjoint diameter edges is the geometric input that keeps ordered shell multiplicity under the $2n$ threshold. The declaration does not itself close Erdős #132; it only converts one geometric packaging into the other so the thrackle and layer hypotheses can fire.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.