erdos132_from_unified_separation_thrackle_and_convex_layer_screening
plain-language theorem explainer
Erdős problem #132 in ordered-pair form follows from four classical bridges: planar segment separation, a unified separated-diameter contradiction, the undirected thrackle support bound, and convex-layer screening. Anyone citing the RS physicalization of distinct sparse distance shells would use this assembly. The proof is a short term application that first builds a four-point diameter-crossing hypothesis, then hands it to the existing four-point thrackle-plus-layer route.
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) no such separation can coexist with two diameter equalities $d(a,b)=d(c,d)=\Delta$ and all four cross-distances $\le\Delta$; (iii) for all large $n$, any ordered edge set on an $n$-point set with no geometrically disjoint pair has undirected support size at most $n$; (iv) for all large $n$, every diameter shell admits convex first/second-layer data screening the deep residual case. Then for all sufficiently large finite planar point sets $A$ there exist distinct distances $r\ne s$ that are both sparse shells of $A$.
background
The module physicalizes Erdős problem #132: a classical distance value is a shell in the pairwise Euclidean spectrum; in RS language 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 multiplicity, so the classical bound $\le n$ becomes $\le 2n$.
A sparse shell is a positive distance whose ordered multiplicity stays at most linear in $|A|$. The target statement asserts that every large enough finite planar set carries at least two distinct sparse shells.
The four hypotheses are pure geometry bridges. Segment separation is the standard planar case split for endpoint-disjoint non-meeting segments (proper orientation versus collinear). The unified separated-diameter contradiction forbids any such certificate when both segments realize the diameter $\Delta$ and all four cross-distances are $\le\Delta$. The thrackle support bound is the Perles/Hopf–Pannwitz undirected form: no geometrically disjoint ordered pairs implies undirected support size $\le|A|$. Convex-layer screening supplies first/second-layer data that kills the residual deep-layer low-shell case for large sets.
proof idea
Term-mode assembly, not a fresh geometric argument. First apply the lemma that turns the segment-separation case split plus the unified separated-diameter contradiction into a four-point diameter-crossing hypothesis (the collinear subcase is already discharged inside that lemma, since the collinear separated-diameter contradiction is a proved theorem). Then feed that crossing hypothesis, together with the undirected thrackle support bound and the convex-layer screening bridge, into the existing four-point thrackle-and-layer assembly theorem, which returns the ordered Erdős #132 statement.
No new case analysis appears here; the work is pure hypothesis wiring.
why it matters
This is the reduced final assembly for the RS reading of Erdős #132 inside DistanceShellMultiplicity. Earlier routes needed a separate collinear separated-diameter contradiction hypothesis; that object is now a theorem, so the collinear branch is automatic and only the unified separated-diameter contradiction remains. The declaration therefore closes the plan's "final assembly" step: sparse-shell existence for large planar sets follows from segment separation, diameter contradiction, thrackle support, and layer screening alone.
In the broader RS picture the result anchors the claim that two-body recognition-energy shells cannot stay uniformly dense: at least two sparse shells must appear. That matches the module's shell-flux reading (and the stronger open target that the number of sparse shells diverges). No downstream Lean consumers are wired yet; the theorem stands as the top-level ordered #132 package for this module. It does not itself invoke the forcing chain T0–T8 or the J-cost functional; those enter only as ambient RS motivation for treating distance shells as recognition-energy levels.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.