erdos132_from_four_point_thrackle_and_convex_layer_screening
plain-language theorem explainer
From four-point diameter crossing, the undirected thrackle support bound, and convex-layer screening, every large enough finite planar point set has two distinct sparse distance shells (ordered Erdős #132). Legacy pre-Conway assembly cited by the thrackle-and-layer and separation-based final packs. One-line term proof: convert screening to a no-deep-layer hypothesis and apply the four-point thrackle bridge.
Claim. Assume: (i) any two endpoint-disjoint diameter pairs in the plane, with all six pairwise distances at most the common diameter $\Delta$, have intersecting closed segments; (ii) for large $n$, any ordered edge set on an $n$-point set with no geometrically disjoint pair has undirected support of size at most $n$; (iii) every large finite planar set admits first/second convex-layer data that screens the low-shell deep-layer residual on a diameter shell. Then for all sufficiently large $n$, every planar $n$-point set has two distinct sparse ordered distance shells.
background
The 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. Ordered pairs are used for Lean bookkeeping: for a positive distance, ordered multiplicity is twice the unordered count, so the classical bound $\le n$ becomes $\le 2n$. The target Erdos132Ordered asserts that large planar sets carry two distinct sparse shells.
The three hypotheses are pure geometric interfaces. Four-point diameter crossing is the $n$-independent Hopf–Pannwitz core: endpoint-disjoint diameter pairs with all cross-distances $\le\Delta$ meet as closed segments. Undirected thrackle support bound is the Perles/Hopf–Pannwitz counting form (no geometrically disjoint pairs implies undirected support $\le|A|$), stated with the set-theoretic meeting predicate that still allows collinear overlaps. Convex-layer screening is the remaining layer-flux theorem: large sets admit layer data that kill the deep-layer residual on a diameter shell.
proof idea
Pure one-line term composition. The convex-layer screening hypothesis is first turned into a no-deep-layer residual statement by no_deep_layer_from_convex_layer_screening. That residual, together with four-point diameter crossing and the undirected thrackle support bound, is fed to erdos132_from_four_point_thrackle_and_no_deep_layer, which already concludes the ordered Erdős #132 statement. No new geometric argument appears at this node.
why it matters
This is the legacy plan-language assembly of the ordered Erdős #132 claim before the Conway correction. The module doc frames the whole development as the RS physicalization of distance-shell multiplicity (two-body recognition-energy shells). Downstream, erdos132_from_thrackle_and_layer specializes it by supplying the proved four-point crossing theorem; the separation-based and unified-separation assemblies reuse the same thrackle-plus-screening spine with stronger diameter-contradiction packages. The live endpoint named in the thrackle-and-layer doc is the Conway-corrected residual pack, so this node is retained mainly for proof-graph comparison. The attached caveat matters: undirected thrackle support as stated permits overlapping collinear segments and is not the correct global counting theorem on collinear configurations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.