erdos132_from_ordered_conway_convex_layer_residual_pack
plain-language theorem explainer
A residual package that bundles ordered Conway thrackle support with convex-layer screening already implies the ordered form of Erdős #132: every large enough finite planar point set has two distinct sparse distance shells. Combinatorial geometers in the RS shell-multiplicity program cite this as the pack-level discharge of the Conway-plus-layer route. The proof is a one-line unpack of the two package fields into the live assembly theorem.
Claim. If a residual package supplies both an ordered Conway thrackle support bound and a convex-layer screening bridge, then Erdős problem #132 holds in ordered-pair normalization: for all sufficiently large $n$, every planar $n$-point set $A$ admits distinct distances $r \neq s$ that are both sparse shells of $A$.
background
This 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 occupancy. The development uses ordered pairs for Lean simplicity: for a positive distance, ordered multiplicity is exactly twice the unordered multiplicity, so the classical threshold $\le n$ becomes $\le 2n$.
The ordered target asserts that, eventually in $n$, every finite planar $n$-point set has two distinct sparse shells. The residual package is the proof-plan object that packages exactly two components: an ordered Conway thrackle support bound (counting control on diameter-type edges) and a convex-layer screening bridge (excluding deep convex layers in the low-shell regime).
Upstream, the live assembly theorem already shows that those two hypotheses imply the ordered Erdős statement, reducing through the eventual no-deep-layer path.
proof idea
Pure term-mode wrapper. Unpack the residual package into its two fields (ordered Conway thrackle support bound and convex-layer screening bridge) and apply the live assembly theorem that takes precisely those two hypotheses and returns the ordered Erdős claim. That live theorem itself routes through the ordered-Conway-plus-eventual-no-deep-layer assembly. No new geometric argument is introduced; the declaration only names the component pair as a residual pack and discharges it.
why it matters
This is the pack-shaped entry point for the Conway-plus-convex-layer residual route in the RS reading of Erdős #132. Downstream consumers include the large non-star current residual discharge and the thrackle-plus-no-deep-layer assembly family, each converting more specialized geometric hypotheses into the same ordered two-sparse-shells claim. In the framework the lemma anchors the combinatorial side of distance-shell multiplicity: occupancy of two-body recognition-energy shells on the plane. It sits entirely on the mathematics track of the shell-flux program and does not engage the T0–T8 forcing chain, the Recognition Composition Law, or the fine-structure residual band around $\alpha^{-1}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.