FourPointDiameterCrossing
plain-language theorem explainer
Any two endpoint-disjoint diameter segments in the Euclidean plane, with all four cross-distances at most the common length Δ, have intersecting closed segments. This is the n-independent four-point geometric core of Hopf–Pannwitz. Downstream Erdős #132 assemblies and the closed four-point theorem cite it as a Prop hypothesis or as the statement proved. The body is a pure universal Prop, not a proof.
Claim. The following property of the plane: for all points $a,b,c,d \in \mathbb{R}^2$ and all $\Delta \in \mathbb{R}$, if the four endpoints are pairwise distinct across the two pairs ($a \neq c$, $a \neq d$, $b \neq c$, $b \neq d$), $\mathrm{dist}(a,b)=\mathrm{dist}(c,d)=\Delta$, and every cross-distance is at most $\Delta$, then the closed segments $[a,b]$ and $[c,d]$ intersect.
background
The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, with ordered-pair multiplicity twice the unordered count (threshold $\le n$ becomes $\le 2n$).
Point2 is the Euclidean plane $\mathbb{R}^2$. Two ordered edges meet geometrically when their closed straight-line segments share a point (the correct Hopf–Pannwitz / thrackle intersection predicate). A diameter shell is a distance value $\Delta$ that realizes the maximum pairwise distance in a finite planar set; here the same bound is imposed only on the six distances among four points, with no ambient finite set.
The definition packages that four-point configuration as a single Prop. It does not depend on $n$ or on any global point set; it is the local geometric engine behind diameter thrackle arguments.
proof idea
No proof: this is a definitional Prop. The body is a single universal quantifier over four plane points and a real $\Delta$, with four endpoint-distinctness hypotheses, two equalities fixing both segments as length $\Delta$, four inequalities bounding the cross-distances by $\Delta$, and conclusion that the ordered edges meet geometrically.
The $\Delta=0$ case is noted immediately below as vacuous (the hypotheses force $a=c$ and $c\neq a$). Actual proofs live in the discharge theorems that inhabit this Prop.
why it matters
This is the universal four-point geometric core behind Hopf–Pannwitz in the RS treatment of Erdős #132. The closed theorem fourPointDiameterCrossing_thm inhabits it; two constructive routes build it from segment-separation plus separated-diameter contradictions (four_point_diameter_crossing_from_separated_diameter, four_point_diameter_crossing_from_separation_bridges).
It feeds the endpoint-disjoint local meeting bridge and the legacy Erdős #132 assemblies that thread four-point geometry through thrackle support and convex-layer / no-deep-layer screening. Downstream docs stress that the four-point diameter geometry is live and proved; only the global counting input was later corrected toward Conway.
In the module's RS reading, diameter shells are recognition-energy shells; this lemma is the local crossing obstruction that caps shell occupancy before global combinatorial bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.