erdos132_from_separation_thrackle_layer
plain-language theorem explainer
Erdős problem #132 in ordered-pair form follows from three geometric bridges: planar segment separation, the undirected thrackle support bound, and convex-layer screening. The four-point Hopf–Pannwitz diameter contradictions are already theorems, so they drop out of the hypothesis list. Discrete geometers working the thrackle/diameter route to #132 would cite this assembly. The proof is a one-line term application of the prior four-hypothesis reducer, plugging in the proved proper-separation contradiction.
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) for all sufficiently large finite $A\subset\mathbb{R}^2$, every ordered edge set on $A$ with no geometrically disjoint pair has undirected support of size at most $|A|$; (iii) every large finite $A$ admits convex-layer data screening the residual deep-layer case of a diameter shell. Then for all sufficiently large finite planar $A$ 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 classical multiplicity $\le n$ becomes ordered multiplicity $\le 2n$.
Erdos132Ordered asserts that every large enough finite planar point set has two distinct sparse shells. The three remaining hypotheses are abstract classical bridges. Segment separation is the standard planar case split (proper orientation vs collinear). The thrackle support bound is the Perles/Hopf–Pannwitz undirected form: no geometrically disjoint ordered pairs implies undirected support size $\le |A|$ (with a documented collinear caveat on the meeting predicate). Convex-layer screening supplies first/second-layer data that kills the residual deep-layer diameter-shell case.
Earlier assembly needed four bridges. Both collinear and proper separated-diameter contradictions are now proved theorems, so the Hopf–Pannwitz four-point core is fully discharged and only the three hypotheses above remain.
proof idea
One-line term wrapper. It applies the prior reducer erdos132_from_proper_separation_thrackle_and_convex_layer_screening, feeding the three open hypotheses together with the already-proved theorem properSeparatedDiameterContradiction in place of the old proper-separation bridge hypothesis. No new geometry is argued here; the reduction is purely assembly once that diameter contradiction is unconditional.
why it matters
This is the further-reduced assembly step for the RS physicalization of Erdős #132 in DistanceShellMultiplicity. The doc-comment records that discharging both Hopf–Pannwitz diameter contradictions collapses the hypothesis surface to segment separation, undirected thrackle support, and convex-layer screening. No downstream consumers are wired yet (used_by is empty), so the declaration is a terminal packaging theorem for the ordered #132 claim rather than an intermediate lemma in a longer chain.
In the broader RS picture the module treats distance shells as recognition-energy shells; the classical sparsity threshold is the occupancy bound that the thrackle and layer-flux geometry must force. The remaining open load sits entirely in the three named bridges (especially global convex-layer screening and the thrackle support bound under the stated meeting predicate), not in four-point diameter algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.