erdos132_from_separation_thrackle_and_convex_layer_screening
plain-language theorem explainer
Erdős #132 in ordered-pair form follows from five planar geometry bridges: segment separation, proper and collinear diameter contradictions, undirected thrackle support, and convex-layer screening. Cite this when reducing the two-sparse-shell claim to Hopf–Pannwitz and layer-flux ingredients. The proof is a short term assembly: package the three separation bridges into a four-point crossing hypothesis, then apply the four-point thrackle-plus-screening theorem.
Claim. Assume: (i) endpoint-disjoint non-meeting segments admit a proper or collinear separation certificate; (ii) proper-separated diameter pairs cannot satisfy all four cross-distance $\le\Delta$ bounds; (iii) collinear-separated diameter pairs force some cross-distance $>\Delta$; (iv) an ordered edge set with no geometrically disjoint pair has undirected support size at most $|A|$ for large $|A|$; (v) every large finite set admits convex first/second-layer data screening the low-shell deep-layer residual. Then for all sufficiently large finite $A\subset\mathbb{R}^2$ there exist distinct distances $r\neq s$ that are both sparse shells of $A$ (ordered multiplicity $\le 2|A|$).
background
This module is the RS physicalization of Erdős problem #132. Classically a distance value is a shell in the pairwise Euclidean spectrum; physically it is a two-body recognition-energy shell, and multiplicity is shell occupancy. The development uses ordered pairs: for a positive distance, ordered multiplicity is twice the unordered count, so the classical threshold $\le n$ becomes $\le 2n$. The target asserts that every sufficiently large finite planar set has two distinct sparse shells.
The five hypotheses are named geometric bridges. Segment separation is the planar case split: endpoint-disjoint non-meeting segments yield a proper orientation or collinear separation certificate. The proper and collinear diameter contradictions are the Hopf–Pannwitz cores: two diameter-length segments that are properly or collinearly separated cannot keep all four cross-distances $\le\Delta$. Undirected thrackle support is the Perles/Hopf–Pannwitz bound. Convex-layer screening supplies first/second-layer data that kills the residual deep-layer low-shell case.
Upstream, the collinear and proper diameter contradictions are already theorems in this module. The immediate parent assembly is the four-point thrackle-plus-screening theorem.
proof idea
Short term-mode assembly. First apply the four-point diameter-crossing construction to the triple of separation hypotheses: the segment-separation case split plus the two diameter contradictions yield the four-point diameter-crossing hypothesis. Then invoke the four-point thrackle-and-convex-layer-screening theorem on that crossing hypothesis together with the undirected thrackle support bound and the convex-layer screening bridge. The result is the ordered Erdős #132 statement. No extra arithmetic appears at this layer.
why it matters
This is the final assembly that packages the full separated-segment bridge decomposition with thrackle support and convex-layer screening into Erdős #132 (ordered form). Downstream, the reduced assembly drops the collinear hypothesis: because the collinear diameter contradiction is already a Lean theorem, Erdős #132 follows from proper separation, the segment case split, thrackle support, and layer screening alone.
In the Recognition framework the claim is the RS reading of distance-shell multiplicity: sparse shells are low-occupancy two-body recognition-energy levels, and two distinct sparse shells for large planar sets is the physicalized Erdős #132 statement. The geometry sits on Hopf–Pannwitz thrackle bounds and convex-layer flux screening, not on the T0–T8 forcing chain. Remaining open load sits in discharging still-hypothetical bridges (segment separation, thrackle support, layer screening), not in this proved assembly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.