erdos132_from_undirected_thrackle_and_no_deep_layer
plain-language theorem explainer
Under four geometric hypotheses (no disjoint diameter edges, undirected thrackle support bound, orientation fibers at most two, and no deep layer in the low-shell regime), every large finite planar point set has two distinct sparse distance shells. Cite this only as the legacy undirected-thrackle assembly of the ordered Erdős #132 statement. The proof is a one-line reduction: convert undirected support plus orientation into the ordered thrackle bound, then apply the thrackle-level final assembly.
Claim. Assume: (i) for large finite $A\subset\mathbb{R}^2$, the diameter-edge graph has no two geometrically disjoint edges; (ii) any ordered edge set with no geometrically disjoint pair has undirected support of size at most $|A|$; (iii) orientation fibers of such edge sets have size at most two; (iv) in the low-shell regime on a diameter shell, the residual deep-layer case never occurs. Then for all sufficiently large finite planar $A$ there exist distinct distances $r\neq 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 it is a two-body recognition-energy shell whose multiplicity is occupancy. Ordered pairs are used for Lean bookkeeping. For positive distances, ordered multiplicity is twice the unordered count, so the classical bound $\le n$ becomes $\le 2n$. The target Erdos132Ordered asserts that every large finite planar set has two distinct sparse shells.
The diameter shell is the unique maximal distance shell. Hopf–Pannwitz geometry enters as NoDisjointDiameterEdges: no two diameter edges are geometrically disjoint. The older thrackle route packages Perles/Hopf–Pannwitz as an undirected support bound (at most $|A|$ undirected edges when no pair is disjoint), plus an orientation-fiber bound (at most two ordered lifts per undirected edge). The residual geometric obstruction after finite accounting is NoDeepLayerCaseInLowShellRegime.
Upstream, the live thrackle-level assembly erdos132_from_thrackle_and_no_deep_layer already concludes the ordered Erdős statement from no-disjoint-diameter, ordered thrackle, and no-deep-layer. This declaration is the legacy front-end that feeds that assembly via undirected support.
proof idea
One-line term wrapper. Apply ordered_thrackle_bound_from_undirected_support to the undirected thrackle support hypothesis and the orientation-fiber bound; that yields the ordered thrackle bound. Pass the no-disjoint-diameter hypothesis, that ordered thrackle bound, and the no-deep-layer hypothesis into erdos132_from_thrackle_and_no_deep_layer, which itself reduces to the diameter-sparsity plus no-deep-layer assembly. No new geometric argument is introduced here.
why it matters
Records the RS-facing ordered form of Erdős #132 along the deprecated undirected-thrackle decomposition. In the framework this is pure mathematics scaffolding for shell multiplicity: sparse shells are the combinatorial shadow of low-occupancy recognition-energy shells on the distance spectrum. The doc-comment is explicit that UndirectedThrackleSupportBound is too strong for arbitrary collinear edge systems and is not the correct Conway thrackle theorem; the preferred live endpoint is erdos132_from_ordered_conway_convex_layer_residual_pack.
No downstream consumers are recorded (used_by empty). Keep the theorem as a conditional historical bridge in the proof graph, not as the citation target for the corrected Conway path. It does not touch T0–T8 forcing, RCL, or the constants ladder; its role is the planar combinatorial lemma behind the shell-flux reading of Erdős #132.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.