four_point_diameter_crossing_zero_case
plain-language theorem explainer
When the common diameter length is zero, any two endpoint-distinct diameter pairs in the plane already contradict the distance axioms: the cross-distance bounds force a pair of endpoints to coincide. The geometric-meeting claim is therefore vacuously true. Cited only as the Δ = 0 branch of the four-point Hopf–Pannwitz crossing theorem. Proof is a one-step ex falso via antisymmetry of distance.
Claim. Let $a,b,c,d\in\mathbb{R}^2$ with $a\neq c$, $a\neq d$, $b\neq c$, $b\neq d$. If $\mathrm{dist}(a,b)=\mathrm{dist}(c,d)=0$ and all four cross-distances $\mathrm{dist}(a,c)$, $\mathrm{dist}(a,d)$, $\mathrm{dist}(b,c)$, $\mathrm{dist}(b,d)$ are at most $0$, 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, and shell multiplicity is occupancy. Ordered pairs are used for Lean bookkeeping; for positive distances ordered multiplicity is twice the unordered count, so the classical bound $\le n$ becomes $\le 2n$.
Points live in the Euclidean plane (Point2 is $\mathbb{R}^2$). Two ordered edges meet geometrically when their closed straight-line segments share a point; that is the Hopf–Pannwitz / thrackle intersection predicate used throughout the module (endpoint-disjointness alone is too strong).
FourPointDiameterCrossing is the $n$-free four-point core: any two endpoint-disjoint pairs of common length $\Delta$, with all six pairwise distances $\le\Delta$, have intersecting closed segments. The present lemma is exactly the $\Delta=0$ specialization of that statement.
proof idea
Pure contradiction. From $\mathrm{dist}(a,c)\le 0$ and non-negativity of Euclidean distance, antisymmetry of $\le$ yields $\mathrm{dist}(a,c)=0$. Equality of distance to zero forces $a=c$, which directly negates the hypothesis $a\neq c$. The remaining hypotheses are unused; the goal (geometric meeting) is discharged by exfalso.
why it matters
Feeds the parent theorem fourPointDiameterCrossing_thm, which closes the full four-point Hopf–Pannwitz crossing statement by case-splitting on whether the common length $\Delta$ vanishes. The zero branch is this lemma; the positive branch carries the genuine planar geometry.
That crossing theorem is the universal four-point geometric core behind the module's attack on Erdős #132 (distance-shell multiplicity / thrackle-type bounds). In the RS reading, diameter shells are maximal two-body recognition-energy shells; forcing diameter pairs to cross constrains how many ordered pairs can sit on a sparse shell. No forcing-chain landmark (T0–T8) is touched directly; the result is pure planar metric geometry supporting the shell-multiplicity program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.