DiameterEdgeSupportFormsConwayThrackle
plain-language theorem explainer
Defines the diameter-shell Conway thrackle condition on unordered edge support: whenever Δ is a diameter shell of a finite planar point set A, the ordered diameter edges form a Conway thrackle support. Cited by the diameter multiplicity bound and by the reduction from simple-representative certificates. Pure propositional packaging; no proof content.
Claim. The following property holds: for every finite set $A$ of points in the Euclidean plane and every real $\Delta$, if $\Delta$ is a diameter shell of $A$, then the ordered diameter edges of $(A,\Delta)$ form a Conway thrackle support (distinct unordered diameter support edges have ordered representatives whose segments meet in exactly one point).
background
The module physicalizes Erdős problem #132: a distance value is a shell in the pairwise Euclidean spectrum, read as a two-body recognition-energy shell whose multiplicity is occupancy. Ordered pairs are used for Lean bookkeeping; for positive distances ordered multiplicity is twice the classical unordered count, so the classical $\le n$ threshold becomes $\le 2n$.
Points live in $\mathbb{R}^2$ (Point2). A diameter shell means $\Delta$ realizes the maximum pairwise distance and the shell is the set of pairs at that distance. The diameter ordered-edge finset collects those pairs with orientation. Conway thrackle support is the geometric crossing condition: distinct support edges have representatives that meet in exactly one point (the local form after stripping ordered-orientation duplicates).
Upstream geometry is planar Euclidean distance geometry only; the thrackle language is the classical Hopf–Pannwitz / Conway counting setup specialized to the diameter shell.
proof idea
Definitional abbreviation of a universal proposition. The body is the quantified implication “diameter shell $\Rightarrow$ Conway thrackle support on diameterOrderedEdges,” with no tactics or lemmas. Downstream theorems discharge or consume the proposition; this declaration only names it.
why it matters
Names the correct diameter Conway hypothesis for the Hopf–Pannwitz counting step in the RS treatment of Erdős #132. Downstream, diameter_conway_bound_from_support_conway combines a general support-level Conway bound with this diameter condition to obtain DiameterConwayThrackleBound (ordered shell multiplicity $\le 2|A|$). Separately, diameter_support_forms_conway_from_simple_representatives shows a local simple-representative certificate is enough to establish the property.
In the module narrative this is the geometric gate between diameter structure (four-point crossing geometry) and the ordered multiplicity bound that matches the classical thrackle target. It does not itself invoke the forcing chain (T0–T8) or RCL; it sits in the combinatorial geometry layer that feeds shell-occupancy estimates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.