erdos132_from_proper_separation_thrackle_and_convex_layer_screening
plain-language theorem explainer
Erdős problem #132 in ordered-pair form follows from four geometric bridges: planar segment separation, the proper (orientation-sign) Hopf–Pannwitz diameter contradiction, the undirected thrackle support bound, and convex-layer screening. Anyone assembling the RS physicalization of sparse distance shells cites this reduced packing. The proof is a one-line wrapper that feeds the already-proved collinear diameter contradiction into the fuller five-hypothesis assembly.
Claim. Assume: (i) any two endpoint-disjoint non-meeting closed segments in the plane admit either a proper orientation separation or a collinear separation certificate; (ii) proper-separated diameter pairs cannot satisfy all four cross-distance bounds $\le\Delta$; (iii) for all large $n$, any ordered edge set on an $n$-point set with no geometrically disjoint pair has undirected support of size at most $n$; (iv) every large finite planar set admits convex-layer data screening the low-shell deep-layer residual. Then for all sufficiently large finite $A\subset\mathbb{R}^2$ there exist two distinct sparse distance shells.
background
The module physicalizes Erdős #132: a classical distance value is a shell in the pairwise Euclidean spectrum; in RS it is a two-body recognition-energy shell whose multiplicity is occupancy. Ordered pairs are used for Lean bookkeeping, so the classical multiplicity threshold $\le n$ becomes $\le 2n$.
Erdos132Ordered asserts that every large enough finite planar point set has two distinct sparse shells. The four hypotheses are abstract bridges: segment separation is the standard planar case split into proper vs collinear certificates; the proper-separated diameter contradiction is the positive-$\Delta$ orientation-sign core of four-point Hopf–Pannwitz geometry (now itself a theorem, but still exposed as a hypothesis here); undirected thrackle support is the Perles/Hopf–Pannwitz bound that a meeting-only ordered edge set has undirected support size $\le|A|$; convex-layer screening supplies first/second-layer data that kills the residual deep-layer low-shell case.
A sibling collinear diameter contradiction has already been promoted to a theorem, so the older five-hypothesis assembly no longer needs that bridge as an open assumption.
proof idea
One-line term wrapper. It applies the fuller assembly erdos132_from_separation_thrackle_and_convex_layer_screening, passing the four open hypotheses unchanged and substituting the proved term collinearSeparatedDiameterContradiction for the collinear-separated diameter bridge. No new geometry is argued here; the reduction is purely that the collinear Hopf–Pannwitz case is already discharged.
why it matters
This is the reduced packing step in the RS reading of Erdős #132 (distance shells as recognition-energy shells). It sits one rung above the further-reduced theorem erdos132_from_separation_thrackle_layer, which additionally discharges the proper-separated diameter bridge and leaves only segment separation, thrackle support, and convex-layer screening. Together these assemblies isolate exactly which classical geometric inputs still need to be supplied for the ordered sparse-shell claim. In the broader RS ledger the result anchors the combinatorial side of shell occupancy before flux and ladder comparisons; it does not itself invoke the forcing chain T5–T8 or the mass ladder, but it is the mathematical substrate those physical readings cite when they treat sparse shells as two-body recognition events.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.