Erdos132OrderedConwayScreeningResidualPack
plain-language theorem explainer
Packages the two residual hypotheses that close the ordered form of Erdős distinct-distances problem #132: the Conway straight-line thrackle support bound, and pointwise deep-layer screening under low-shell structure. Anyone citing the live classical residual route to the ordered multiplicity bound will name this pack. It is a pure Prop structure with no proof body; discharge is deferred to the two component certificates.
Claim. The residual package for the ordered Erdős #132 claim is the conjunction of (i) the Conway straight-line thrackle support bound (every finite straight-line thrackle on a point set $A$ has undirected support of size at most $|A|$) and (ii) the pointwise deep-layer screening certificate (on any diameter shell $\Delta$ with low-shell structure, deep-layer screening holds, forcing a second sparse shell).
background
The module physicalizes Erdős problem #132: classically a distance value is a shell in the pairwise Euclidean spectrum; here it is a two-body recognition-energy shell whose occupancy is the shell multiplicity. Ordered pairs are used for Lean simplicity, so for positive distances the ordered multiplicity is twice the unordered one and the classical threshold $\le n$ becomes $\le 2n$.
The first packed hypothesis is the Conway straight-line thrackle support bound: if every pair of edges meets simply, the undirected support has at most $|A|$ edges (the Lovász–Pach–Szegedy / Cairns–Nikolayevsky counting theorem). The bound fails without the simple-meeting condition.
The second is the pointwise positive screening form of the layer residual. Under the low-shell hypotheses on a diameter shell $\Delta$, any residual deep-layer case produces the missing second sparse shell, matching the proof plan's Deep-Layer Screening Lemma.
proof idea
No proof body: the declaration is a Prop-valued structure whose fields are exactly the two residual certificates. Instantiating it means supplying a proof of the Conway thrackle support bound and a proof of pointwise deep-layer screening. Downstream, the one-line consumer theorem unpacks the two fields and feeds them to the live bridge erdos132_from_ordered_conway_and_deep_screening_live.
why it matters
This is the current live residual package in standard classical form for the RS physicalization of Erdős #132. Its sole consumer is erdos132_from_ordered_conway_screening_residual_pack, whose doc-comment states that the Conway-counting plus deep-screening residual package proves the ordered Erdős #132 claim. Naming the pack keeps the residual interface stable while the two component certificates are discharged or refined. In the broader Recognition setting, distance shells are two-body recognition-energy shells; closing the multiplicity bound is the combinatorial half of that physicalization. The pack does not itself touch the forcing chain (T0–T8) or the alpha residual, but it is the mathematics-side gate for the ordered shell-occupancy theorem the module records.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.