segments_meet_of_orient2_zero
plain-language theorem explainer
If c is collinear with a diameter segment [a,b] of length Δ and lies in the diameter lens (within Δ of both a and b), then the closed segments [a,b] and [c,d] intersect at c. Combinatorial geometers treating the Hopf–Pannwitz / thrackle side of Erdős #132 cite this meeting lemma. The proof is a two-line refine: witness the intersection at c, then apply the lens-collinearity lemma and left-endpoint-on-segment.
Claim. Let $a,b,c,d$ be points in the plane and $\Delta>0$. Suppose $\mathrm{dist}(a,b)=\Delta$, $\mathrm{dist}(a,c)\le\Delta$, $\mathrm{dist}(b,c)\le\Delta$, and the planar orientation $\mathrm{orient}_2(a,b,c)=0$ (so $c$ is collinear with $a$ and $b$). Then the closed straight-line segments $[a,b]$ and $[c,d]$ intersect.
background
The module records the Recognition Science physicalization of Erdős problem #132. Classically a distance value is a shell in the pairwise Euclidean spectrum; physically it is a two-body recognition-energy shell whose occupancy is the multiplicity. Ordered pairs are used for Lean simplicity: for positive distances, ordered multiplicity is twice the unordered count, so the classical threshold $\le n$ becomes $\le 2n$.
Points live in the plane (Point2). Two ordered edges meet geometrically when their closed segments share a point: there exists $x$ on both closed segments. The diameter lens of a segment of length $\Delta$ is the intersection of the two closed disks of radius $\Delta$ about the endpoints. Vanishing planar orientation encodes collinearity. Any point that is collinear with the segment and inside that lens necessarily lies on the closed segment itself.
proof idea
Term-mode refine builds the existential witness for geometric meeting as the point $c$. The second conjunct is immediate: $c$ is the left endpoint of the ordered edge $(c,d)$, so it lies on that closed segment by the sibling fact left_endpoint_on_segment. The first conjunct (that $c$ lies on $[a,b]$) is discharged by onClosedSegment_of_orient2_zero_in_lens, which packages the full diameter-lens package: $\Delta>0$, exact distance $ab=\Delta$, both $ac$ and $bc$ at most $\Delta$, and vanishing orientation.
why it matters
Infrastructure for the geometric side of the RS treatment of Erdős #132 (distance-shell multiplicity). Diameter representatives that share a left endpoint and stay collinear inside the lens must meet simply at that endpoint; a second intersection would force the free endpoints onto the same diameter segment and hence coincide (the remark immediately below the proof). No recorded downstream uses yet, so the lemma feeds local uniqueness and thrackle-type arguments about diameter shells (IsDiameterShell, isDiameterShell_unique, sparse-shell flux bridges) rather than a named parent theorem. It is pure planar geometry; the D=3 / eight-tick forcing chain is upstream context for the broader recognition stack, not a direct consumer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.