erdos132_from_current_live_residual
plain-language theorem explainer
Assuming the current live residual (a Conway thrackle support bound together with a convex-layer screening bridge), every sufficiently large finite planar point set has two distinct sparse distance shells. Discrete geometers and Recognition Science auditors tracking the Erdős #132 physicalization would cite this. The proof is a one-line unpacking of that residual conjunction into the final assembly lemma.
Claim. If the Conway thrackle support bound and the convex-layer screening bridge both hold, then Erdős problem #132 holds in ordered-pair normalization: for every sufficiently large $n$, every planar $n$-point set $A$ admits two distinct distances $r \neq s$ that are sparse shells of $A$.
background
This module records the Recognition Science physicalization of Erdős problem #132. Classically a distance value is a shell in the set of pairwise Euclidean distances; physically it is a two-body recognition-energy shell, and its multiplicity is the shell occupancy. Ordered pairs are used for Lean simplicity: for a positive distance, ordered multiplicity is exactly twice the usual unordered multiplicity, so the classical threshold $\le n$ becomes $\le 2n$.
A sparse shell is a distance whose ordered multiplicity stays below that linear threshold. The ordered target asserts that for all large enough $n$, every $n$-point planar set carries at least two distinct sparse shells.
The hypothesis is the current live two-input residual: all finite accounting, diameter geometry, ordered/unordered representative bookkeeping, and the support-level Conway correction have already been discharged above, leaving only the conjunction of a Conway thrackle support bound with a convex-layer screening bridge.
proof idea
One-line term proof. The residual is a conjunction; its two projections are passed to the final assembly lemma, which states that standard ordered Conway counting plus convex-layer screening proves the ordered form of Erdős #132. That assembly itself reduces to an eventual no-deep-layer form under the Conway bound, so this declaration is only the residual packaging step.
why it matters
This is the current live endpoint for the RS physicalization of Erdős #132: once the two residual inputs are granted, the ordered form of the problem is proved. It sits at the top of the Distance Shell Multiplicity development, packaging everything already discharged (finite accounting, diameter uniqueness, representative bookkeeping, Conway support correction) into a single two-input residual. No downstream consumers are recorded; the declaration is the present closure point of the proof plan rather than a lemma feeding a larger theorem. In the broader framework it converts a classical discrete-geometry question into a recognition-energy shell-occupancy statement, matching the module's two-body shell reading. The stronger sparse-shells-diverge target suggested by the shell-flux reading remains separate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.