EndpointDisjointDiameterIntersectionUniqueCertificate
plain-language theorem explainer
Certificate Prop: two endpoint-disjoint diameter representatives in a finite planar set meet in at most one point. Existence of a meeting is already supplied elsewhere; this isolates uniqueness. Cited by the Conway-form Erdős #132 assembly and by the simple-meeting reduction for diameter edges. Pure interface definition, discharged downstream from a two-point collinearity hypothesis.
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$ whose underlying unordered edges are distinct and which share no endpoint, then the closed segments of $e$ and $f$ have at most one common point: any $x,y$ lying on both segments must satisfy $x=y$.
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 multiplicity is shell occupancy. Ordered pairs are used for Lean simplicity, so the classical multiplicity bound $\le n$ becomes $\le 2n$.
Points live in the Euclidean plane (Point2). The ordered diameter-edge set collects ordered pairs from $A$ at distance exactly $\Delta$. A diameter shell means $\Delta$ realizes the diameter of $A$. The certificate is uniqueness-only: existence of an intersection of two diameter representatives is already supplied by the four-point diameter crossing theorem; here one only asserts that endpoint-disjoint representatives cannot share two distinct points.
proof idea
Definitional Prop, not a proved theorem. The body is a single universal quantification: over finite planar sets, diameter shell values, pairs of ordered diameter edges that are unordered-distinct and endpoint-disjoint, and pairs of candidate intersection points on both closed segments, concluding the two points coincide. No tactics or lemmas are applied at this site; discharge happens downstream.
why it matters
This is the residual geometric content after the shared-endpoint diameter case is closed. Downstream, the collinearity-forcing hypothesis yields the certificate, which with the four-point crossing theorem gives simple meeting of endpoint-disjoint diameter representatives. The certificate is packed into the live residual structure alongside support-level Conway thrackle bounds and pointwise deep-layer screening, and is a direct hypothesis of the corrected Conway-form assembly that concludes the ordered form of Erdős #132. In the RS reading, diameter shells are the extremal two-body recognition-energy shells whose occupancy must stay sparse.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.