segments_meet_of_opposite_sides
plain-language theorem explainer
In the plane, if ab is a diameter of length Δ and the four cross-distances from {a,b} to {c,d} are at most Δ, with c and d strictly on opposite sides of the line through ab, then the closed segments [a,b] and [c,d] intersect. Cited by the four-point Hopf–Pannwitz crossing theorem in the Erdős #132 shell-multiplicity development. The proof builds an explicit convex-combination point on [c,d] that lies on the line ab and stays inside the Δ-ball of both endpoints.
Claim. Let $a,b,c,d\in\mathbb{R}^2$ and $\Delta>0$ with $\mathrm{dist}(a,b)=\Delta$. Suppose $\mathrm{dist}(a,c),\mathrm{dist}(a,d),\mathrm{dist}(b,c),\mathrm{dist}(b,d)\le\Delta$, and the oriented areas of triangles $abc$ and $abd$ have opposite strict signs. Then the closed segments $[a,b]$ and $[c,d]$ intersect in $\mathbb{R}^2$.
background
The module DistanceShellMultiplicity is the Recognition Science physicalization of 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 the ordered multiplicity is twice the unordered one, so classical thresholds $\le n$ become $\le 2n$.
Point2 is the planar point type from the bipartite distance spectrum. Geometric meeting of ordered edges means the closed straight-line segments share a point: there exists $x$ on both closed segments. That is the correct Hopf–Pannwitz / thrackle predicate; mere endpoint-disjointness would wrongly exclude crossing diameter diagonals.
The signed quantity orient2 a b p is the usual 2D orientation (twice signed area of triangle $abp$). Opposite strict sides of line $ab$ means the product of orientations at $c$ and $d$ is negative. Diameter cross-distance bounds say every leg from ${a,b}$ to ${c,d}$ is at most the diameter length $\Delta=\mathrm{dist}(a,b)$.
proof idea
From $u\cdot v<0$ with $u=\mathrm{orient2}(a,b,c)$ and $v=\mathrm{orient2}(a,b,d)$, both factors are nonzero (else the product vanishes). Set $t=u/(u-v)$. Case analysis on the signs of $u$ and $v$ (via trichotomy and the opposite-sign hypothesis) yields $0<t<1$; the identity $t-1=v/(u-v)$ handles the upper bound.
Form $P=(1-t)c+t,d$. Then $P$ lies on the closed segment $[c,d]$. Affine linearity of orientation (orient2_affine_third) plus field simplification gives $\mathrm{orient2}(a,b,P)=0$, so $P$ is on the line through $ab$. Convex-combination distance bounds (dist_convex_combination_le) keep $\mathrm{dist}(a,P)\le\Delta$ and $\mathrm{dist}(b,P)\le\Delta$. With $\mathrm{dist}(a,b)=\Delta$ and $P$ collinear with $a,b$, those inequalities force $P$ onto the closed segment $[a,b]$. The common point $P$ witnesses geometric meeting.
why it matters
This is the opposite-sides geometric engine for the closed four-point Hopf–Pannwitz crossing theorem (fourPointDiameterCrossing_thm): if two segments are both of length $\Delta$, all four cross-distances are $\le\Delta$, and the four endpoints are pairwise distinct across the two segments, then the closed segments meet. The parent theorem case-splits on $\Delta=0$ and on relative orientation; the strict opposite-sides branch lands here.
In the Erdős #132 development, diameter crossings control when sparse distance shells can avoid thrackle-type intersections. That feeds the shell-multiplicity bounds that physicalize the classical problem as recognition-energy shell occupancy. The argument is pure planar Euclidean geometry; it does not itself invoke the forcing chain (T0–T8) or the Recognition Composition Law, but it sits inside the mathematics layer those physical claims rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.