DistinctDiameterRepresentativesMeetSimply
plain-language theorem explainer
Any two ordered diameter edges of a finite planar point set that realize distinct unordered support edges meet in exactly one vertex. Diameter-shell analysts and anyone discharging the ordered Conway certificate on the diameter side cite this interface. It is a pure Prop definition packaging the ordered-representative form of the diameter-support meeting condition; no proof is attached.
Claim. For every finite set $A$ of points in the plane and every real $\Delta$ that is a diameter shell of $A$, if $e$ and $f$ are ordered diameter edges of $A$ at distance $\Delta$ whose underlying unordered edges are distinct, then $e$ and $f$ meet in exactly one point.
background
The module physicalizes Erdős problem #132 inside Recognition Science: a classical distance value is a shell in the pairwise Euclidean spectrum; physically it is a two-body recognition-energy shell whose occupancy is the shell multiplicity. Ordered pairs are used for Lean bookkeeping; for positive distances the ordered multiplicity is exactly twice the unordered one, so classical thresholds double.
A diameter shell is a distance shell realizing the global maximum pairwise distance of a finite point set $A\subset\mathbb{R}^2$. The ordered diameter edges are the oriented pairs in $A\times A$ at that distance. Forgetting orientation yields the unordered support edge. Two ordered edges meet simply when they share exactly one endpoint (no full coincidence, no empty intersection).
The definition packages the sharp local geometry left on the diameter side of the Conway-type support condition: distinct unordered diameter supports force simple meeting of any chosen ordered representatives.
proof idea
No proof body: the declaration is a Prop abbreviation. It universally quantifies over finite point sets $A$, candidate diameters $\Delta$, a diameter-shell hypothesis, and pairs of ordered diameter edges whose unordered images differ, then asserts the simple-meeting predicate on that ordered pair. Downstream lemmas discharge or consume the packaged statement; the definition itself only names the target.
why it matters
This is the ordered-representative form of the diameter-support Conway condition, the sharp local geometry retained on the diameter side of the shell-multiplicity program. It feeds two immediate parents: the case-split theorem that builds the full ordered certificate from shared-endpoint and endpoint-disjoint lemmas, and the support-level bridge that, given this Prop, chooses ordered lifts of two unordered support edges and obtains the unordered simple-representative certificate.
In the broader RS reading of Erdős #132, diameter shells are the extremal two-body recognition-energy shells; controlling how their representatives meet is the combinatorial gate before multiplicity and flux bridges. The definition removes the orientation-duplicate pathology so later arguments never double-count reverse edges as distinct supports.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.