DiameterSupportSimpleRepresentativeCertificate
plain-language theorem explainer
Names the local geometric certificate that, on any diameter shell, distinct unordered support edges have ordered representatives meeting in exactly one point. Combinatorial geometers working the RS form of Erdős #132 cite it as the orientation-free Conway thrackle condition on the diameter side. Pure Prop packaging: no proof content, only the quantified statement later discharged or applied.
Claim. For every finite planar point set $A$ and every real $\Delta$, if $\Delta$ is a diameter shell of $A$, then any two distinct unordered edges in the diameter support of $A$ at distance $\Delta$ admit ordered representatives whose segments 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, so positive-distance ordered multiplicity is twice the unordered count and classical thresholds double.
A diameter shell is the (unique, nonnegative) shell realizing the maximum pairwise distance of a finite set $A\subset\mathbb{R}^2$. The diameter ordered-edge list collects all ordered pairs in $A$ at that distance; its unordered edge support forgets orientation. The simple-meeting predicate on support edges asserts that chosen ordered representatives intersect in exactly one point (the local Conway thrackle geometry).
This definition isolates that geometry after orientation duplicates are removed: it is the residual local condition on distinct unordered diameter support edges.
proof idea
Definitional packaging only. The body is the universal quantification over finite point sets $A$, candidate distances $\Delta$, the diameter-shell hypothesis, and pairs of distinct members of the unordered diameter support, concluding the simple-meeting predicate on the diameter ordered-edge list. No tactics, no lemmas applied.
why it matters
Sits on the diameter side of the RS reading of Erdős #132, where shell multiplicity and support geometry constrain two-body recognition energy. Downstream, the one-line wrapper diameter_support_forms_conway_from_simple_representatives shows the certificate is exactly enough to conclude that diameter edge support forms a Conway thrackle. The companion diameter_support_simple_representatives_from_ordered_representatives lifts the ordered-representative simple-meeting hypothesis to this support-level certificate by choosing representatives of the two unordered edges. Together they separate orientation bookkeeping from the sharp local geometry left on the diameter support.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.