erdos132_from_thrackle_and_layer
plain-language theorem explainer
Assuming the undirected thrackle support bound and the convex-layer screening bridge, every sufficiently large finite planar point set has two distinct sparse distance shells (Erdős #132 in ordered-pair form). Discrete geometers on the thrackle/Hopf–Pannwitz route to #132 would cite this reduced assembly. The proof is a one-line term application that feeds the closed four-point diameter-crossing theorem into the legacy four-point thrackle-plus-layer assembly. It is retained only as a pre-Conway-correction checkpoint.
Claim. If the undirected thrackle support bound holds (any ordered edge set on $A$ with no geometrically disjoint pairs has undirected support of size at most $|A|$) and the convex-layer screening bridge holds (every large finite planar set admits first/second layer data that screens the low-shell residual deep-layer case), 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$.
background
The module records 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 whose multiplicity is shell occupancy. Ordered pairs are used for Lean simplicity: for a positive distance, ordered multiplicity is twice the unordered count, so the classical threshold $\le n$ becomes $\le 2n$.
The conclusion is the ordered form of #132: every sufficiently large finite planar set admits two distinct sparse distance shells. A sparse shell is a distance whose ordered multiplicity stays linearly bounded in $|A|$.
The first hypothesis is the undirected thrackle support bound (Perles/Hopf–Pannwitz in clean undirected form), with the documented caveat that the set-theoretic meeting predicate allows overlapping collinear segments and fails on collinear point sets. The second is global convex-layer screening: large sets admit first/second layer data screening the deep-layer residual. Upstream, the four-point diameter-crossing theorem is already closed: equal-diameter segments whose four cross-distances are at most the diameter must meet geometrically.
proof idea
One-line term wrapper. It applies the legacy assembly that derives the ordered #132 statement from a four-point diameter-crossing hypothesis, the undirected thrackle support bound, and convex-layer screening, supplying the already-proved four-point diameter-crossing theorem as the first argument together with the two named hypotheses. That assembly itself reduces to the no-deep-layer route under those geometric inputs. No new combinatorial argument is introduced here.
why it matters
Legacy reduced assembly retained for comparison with the pre-Conway-correction proof graph. The live final endpoint is the ordered Conway convex-layer residual pack theorem named in the doc-comment. In the RS reading of Erdős #132, this packages the thrackle-plus-layer path that turns geometric support bounds and layer-flux screening into two sparse recognition-energy shells on the distance spectrum. No downstream consumers are recorded; the declaration is a historical checkpoint, not a live dependency. The thrackle hypothesis still carries the collinear-set caveat that motivated the Conway correction, so this path is not the unconditional end of the story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.