erdos132_from_conway_endpoint_disjoint_uniqueness_screening_residual_pack
plain-language theorem explainer
A residual certificate pack (support-level Conway thrackle bound, endpoint-disjoint diameter intersection uniqueness, and pointwise deep-layer screening) implies Erdős #132 in ordered-pair form: every large enough finite planar point set has two distinct sparse distance shells. Cite when assembling the live RS proof of #132 after the shared-endpoint diameter case is closed. Proof is a one-line term application of the live Conway-form assembly lemma to the three pack fields.
Claim. Suppose a residual package supplies (i) a Conway thrackle support bound on the support, (ii) an endpoint-disjoint diameter intersection uniqueness certificate, and (iii) a pointwise deep-layer screening certificate. Then Erdős problem #132 holds in ordered-pair normalization: for all 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 physicalizes Erdős problem #132 inside Recognition Science. Classically a distance value is a shell in the pairwise Euclidean distance set; here it is a two-body recognition-energy shell, and multiplicity is shell occupancy. The development uses ordered pairs for Lean simplicity: for a positive distance, ordered multiplicity is twice the unordered multiplicity, so the classical threshold $\le n$ becomes $\le 2n$.
Erdős #132 (ordered) asserts that for every sufficiently large finite planar set there exist two distinct sparse distance shells. The residual pack is the live package left after the shared-endpoint diameter representative case is closed. Its three fields are a support-level Conway thrackle bound, an endpoint-disjoint diameter intersection uniqueness certificate, and a pointwise deep-layer screening certificate.
Upstream, the live Conway-form assembly states that those three hypotheses already imply the ordered Erdős claim, with the shared-endpoint case handled separately and endpoint-disjoint existence supplied by a four-point diameter crossing theorem.
proof idea
One-line term wrapper. Unpack the three fields of the residual pack and feed them to the live assembly theorem erdos132_from_support_conway_endpoint_disjoint_uniqueness_and_deep_screening_live, which itself reduces to the diameter-sparsity-plus-no-deep-layer route. No extra algebraic work occurs at this node.
why it matters
This is the live final assembly node for the endpoint-disjoint uniqueness residual path to Erdős #132 in the RS distance-shell reading. The module frames #132 as a statement about sparse two-body recognition-energy shells; ordered multiplicity doubles the classical count, so the sparse threshold is $\le 2n$. Downstream use sites are not yet wired in this graph snapshot, so the declaration currently stands as a terminal proved bridge from the residual pack to the ordered claim.
It sits after the shared-endpoint diameter representatives are already known to meet simply, and after four-point diameter crossing supplies endpoint-disjoint existence. The pack therefore isolates what remains: Conway support counting, uniqueness of endpoint-disjoint diameter intersections, and pointwise deep-layer screening. Closing those three certificates discharges the ordered Erdős statement along this residual route.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.