fourPointDiameterCrossing_thm
plain-language theorem explainer
Any two endpoint-disjoint diameter segments in the plane, with all six pairwise distances at most the common length Δ, have intersecting closed segments. This is the n-independent geometric core of the Hopf–Pannwitz theorem and the four-point engine behind the module’s attack on Erdős #132. The proof splits on Δ = 0, then exhausts orientation signs of the two free points relative to the first diameter, routing each case to a same-side, opposite-side, collinear, or endpoint-meeting lemma.
Claim. For all points $a,b,c,d\in\mathbb{R}^2$ and all $\Delta\in\mathbb{R}$, if the cross-endpoint pairs are distinct ($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 among $\{a,b\}\times\{c,d\}$ is at most $\Delta$, then the closed segments $[a,b]$ and $[c,d]$ meet geometrically.
background
The module physicalizes Erdős problem #132: a distance value is a shell in the pairwise Euclidean spectrum, read as a two-body recognition-energy shell whose multiplicity is occupancy. Ordered pairs are used for Lean bookkeeping; for positive distances ordered multiplicity is twice the unordered count, so classical bounds $\le n$ become $\le 2n$.
FourPointDiameterCrossing is the universal four-point geometric core behind Hopf–Pannwitz: it does not depend on $n$ or on any ambient finite set. It asserts that any two endpoint-disjoint diameter pairs in the plane, with all six pairwise distances bounded by the diameter, have intersecting closed segments.
Supporting pieces include the vacuous zero-diameter case (hypotheses force $a=c$ and $a\neq c$), collinear separated-diameter contradictions, and orientation/lens lemmas that detect when a third point lies on a diameter segment or when opposite-side orientations force a transversal intersection.
proof idea
Introduce the four points, $\Delta$, distinctness, equal diameters, and cross-distance bounds. Case on $\Delta=0$: discharge by four_point_diameter_crossing_zero_case.
For $\Delta>0$, assume the ordered edges are geometrically disjoint and derive a contradiction. Build two local facts: vanishing orientation of $c$ (resp. $d$) relative to line $ab$ places that point on the closed segment $[a,b]$ inside the diameter lens, hence the edges meet at an endpoint.
Trichotomize orient2 a b c and, in each branch, orient2 a b d. Same-sign nonzero orientations give a positive product and invoke sameSideDiameterContradiction. Opposite signs give a negative product and invoke segments_meet_of_opposite_sides, contradicting disjointness. A zero orientation forces an endpoint meeting. Both orientations zero routes to collinearSeparatedDiameterContradiction.
why it matters
This closes the four-point Hopf–Pannwitz crossing statement as a proved theorem, the geometric engine for diameter-shell arguments in the Erdős #132 development. Downstream, endpoint_disjoint_diameter_representatives_meet_simply_from_unique_live combines it with endpoint-disjoint uniqueness to obtain simple meeting of diameter representatives; the property EndpointDisjointDiameterRepresentativesMeetSimply is the corresponding interface.
It is also fed directly into the legacy assembly erdos132_from_thrackle_and_layer, which builds the ordered Erdős #132 claim from thrackle support and convex-layer screening via the four-point crossing theorem. In the Recognition Science reading, diameter shells are maximal two-body recognition-energy shells; forcing geometric crossing of endpoint-disjoint diameter pairs constrains shell occupancy and underwrites the multiplicity bounds the module targets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.