DiameterConwayThrackleBound
plain-language theorem explainer
Defines the diameter-specific ordered thrackle bound: whenever Δ is a diameter shell of a finite planar point set A, the ordered multiplicity of Δ is at most twice |A|. Workers on the RS physicalization of Erdős #132 and on Hopf–Pannwitz counting cite this Prop as the classical target. It is a pure proposition definition, not a proved theorem; discharge comes from support-level Conway plus diameter geometry.
Claim. The following statement holds as a named proposition: for every finite set $A$ of points in the plane and every real number $\Delta$, if $\Delta$ is a diameter shell of $A$, then the ordered shell multiplicity of $\Delta$ in $A$ satisfies $\mathrm{mult}^{\mathrm{ord}}(A,\Delta)\le 2|A|$.
background
This module physicalizes Erdős problem #132: a classical distance value is a shell in the pairwise Euclidean spectrum; in RS it is a two-body recognition-energy shell, and multiplicity is shell occupancy. The development uses ordered pairs for Lean simplicity. For a positive distance, ordered multiplicity is exactly twice the unordered multiplicity, so the classical threshold $\le n$ becomes $\le 2n$.
A diameter shell is a distance shell whose value equals the diameter of the finite point set (every pair realizing $\Delta$ is a diametral segment). The ordered shell multiplicity counts ordered pairs at that distance. The Conway thrackle condition is the combinatorial crossing restriction that Hopf–Pannwitz-type arguments use to bound how many equal-length edges a planar geometric graph can carry.
The doc-comment stresses that diameter geometry forces the Conway condition via four-point crossing geometry, making this the correct classical target for the Hopf–Pannwitz counting step. A sibling warning notes that a purely ordered-edge thrackle formulation is false (both $(a,b)$ and $(b,a)$ share one segment); the support-level formulation is the one that should be used upstream.
proof idea
No proof: this is a def equating a name to a universal proposition. The body quantifies over finite planar point sets $A$ and reals $\Delta$, assumes the diameter-shell predicate, and asserts the ordered-multiplicity inequality $\le 2|A|$.
Discharge is external. Downstream, diameter_conway_bound_from_support_conway builds an inhabitant from a support-level Conway thrackle bound together with the diameter-edge-support Conway hypothesis, by specializing to a diameter shell and reading off the ordered count. A further one-step filter then turns any such inhabitant into the ordinary diameter-shell sparsity component used by the Erdős #132 assembly.
why it matters
In the Erdős #132 pipeline this Prop is the diameter-specific counting target that Hopf–Pannwitz thrackle geometry is meant to hit. It is consumed in two places in the same module: first as the conclusion of the support-to-diameter Conway transfer (diameter_conway_bound_from_support_conway), and second as the hypothesis of diameter_shell_sparse_from_diameter_conway_bound, whose doc-comment states that the diameter-specific Conway bound implies the ordinary diameter shell sparsity component used by the Erdős #132 assembly.
Within Recognition Science the shell is a two-body recognition-energy level; bounding its occupancy is the combinatorial half of the physicalization. The module keeps ordered multiplicity so the classical $\le n$ bound appears as $\le 2n$. The declaration does not itself close the thrackle step; it names the claim that the diameter geometry plus Conway support are supposed to prove.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.