EndpointDisjointTwoPointIntersectionForcesCollinear
plain-language theorem explainer
Two endpoint-disjoint diameter segments that share two distinct points must be collinear: both endpoints of the second lie on the line through the first. This is the pure affine-incidence certificate behind endpoint-disjoint uniqueness for diameter shells in the Erdős #132 formalization. Anyone assembling the Conway/thrackle residual pack or the live Erdos132Ordered assembly cites it. The declaration is a Prop definition; a companion theorem proves it by orientation vanishing on closed segments.
Claim. For every finite $A \subset \mathbb{R}^2$ and every real $\Delta$ that is a diameter shell of $A$, if $e$ and $f$ are ordered diameter edges at distance $\Delta$, distinct as unordered edges and sharing no endpoint, and if two distinct points $x,y$ both lie on the closed segment of $e$ and of $f$, then both endpoints of $f$ are collinear with the line through $e$ (the planar orientations vanish).
background
The module Distance Shell Multiplicity records the RS physicalization of Erdős problem #132. Classically a distance value is a shell in the set of pairwise Euclidean distances; physically it is a two-body recognition-energy shell whose multiplicity is shell occupancy. Ordered pairs are used for Lean simplicity: for positive distance, ordered multiplicity is twice the unordered count, so the classical threshold $\le n$ becomes $\le 2n$.
Points live in Point2, the Euclidean plane $\mathbb{R}^2$. A diameter shell means $\Delta$ realizes the maximum pairwise distance in the finite set $A$; the diameter ordered edges are the ordered pairs at that distance. Closed-segment membership and planar orientation are the affine incidence primitives: vanishing orientation means collinearity.
The doc-comment isolates this Prop as "the only remaining geometric content behind endpoint-disjoint uniqueness": two distinct common points on two endpoint-disjoint diameter representatives force the second representative's endpoints onto the line of the first.
proof idea
This declaration is a Prop definition (a named geometric certificate), not a proved theorem. The companion theorem endpoint_disjoint_two_point_intersection_forces_collinear discharges it.
That proof introduces the finite set, diameter shell hypothesis, and two ordered diameter edges, then destructs the edge pairs. For each of the two distinct common points it applies the lemma that a point on a closed segment has vanishing orientation with the segment endpoints. Two distinct points determine a unique line, so both endpoints of the second edge also have vanishing orientation against the first edge. The argument is pure affine incidence; no metric estimates beyond the diameter-shell and endpoint-disjoint hypotheses are used.
why it matters
Downstream, endpoint_disjoint_diameter_intersection_unique_from_two_point_collinear takes this Prop as hypothesis and concludes the endpoint-disjoint diameter intersection uniqueness certificate: otherwise the sharper collinear diameter endpoint contradiction applies.
It is bundled in Erdos132ConwayEndpointDisjointCollinearityScreeningResidualPack as the live collinearity field after reducing endpoint-disjoint uniqueness to the two-point certificate. The live final assembly erdos132_from_support_conway_endpoint_disjoint_collinear_and_deep_screening_live consumes this Prop together with a Conway thrackle support bound and pointwise deep-layer screening to obtain Erdos132Ordered.
In the RS reading of Erdős #132, distance shells are two-body recognition-energy shells; this certificate peels the last pure geometry step off the uniqueness argument so combinatorial screening can close the residual pack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.