Erdos132ConwayEndpointDisjointUniquenessScreeningResidualPack
plain-language theorem explainer
Bundles three residual certificates (Conway thrackle support bound, endpoint-disjoint diameter intersection uniqueness, and pointwise deep-layer screening) into one Prop package. Anyone citing the live residual route to the ordered Erdős #132 multiplicity bound uses this pack. There is no proof body: it is a structure of hypotheses discharged downstream.
Claim. A residual package is a triple of propositions: (1) for any finite point set $A\subset\mathbb{R}^2$ and ordered edge set $E$ that is a Conway thrackle support on $A$, the unordered support has size at most $|A|$; (2) on any diameter shell of value $\Delta$, two endpoint-disjoint diameter representatives intersect in at most one point; (3) under low-shell structure on a diameter shell, deep-layer screening holds (any residual deep-layer configuration forces a second sparse shell).
background
The module physicalizes Erdős problem #132: a classical distance value is a shell in the pairwise Euclidean spectrum; in RS it is a two-body recognition-energy shell whose occupancy is the multiplicity. Ordered pairs are used for Lean bookkeeping, so the classical bound $\le n$ becomes $\le 2n$ on ordered multiplicity.
After the shared-endpoint diameter-representative case is closed, three residuals remain. The Conway thrackle support bound is the ordered-finset form of the straight-line thrackle inequality: unordered support size $\le |A|$. The endpoint-disjoint uniqueness certificate is uniqueness-only geometry (existence of a crossing already comes from the four-point diameter crossing theorem): two distinct unordered diameter edges that share no endpoint meet in at most one point. Pointwise deep-layer screening is the positive form of the Deep-Layer Screening Lemma: under low-shell hypotheses on a diameter shell, residual deep-layer configurations produce the missing second sparse shell.
The pack is the live residual surface after those closures; it does not itself assert the thrackle, uniqueness, or screening theorems, only their conjunction as a single Prop.
proof idea
No proof: the declaration is a structure extending Prop with three fields. Each field is a named certificate Prop already defined in-module (ConwayThrackleSupportBoundOnSupport, EndpointDisjointDiameterIntersectionUniqueCertificate, PointwiseDeepLayerScreeningCertificate). Instantiating the pack means supplying proofs of those three Props; the structure merely names the residual interface consumed by the downstream implication to ordered Erdős #132.
why it matters
This is the residual interface for the live path to ordered Erdős #132 in the distance-shell multiplicity development. The parent theorem erdos132_from_conway_endpoint_disjoint_uniqueness_screening_residual_pack takes any instance of the pack and concludes Erdos132Ordered by applying the support-Conway plus endpoint-disjoint uniqueness plus deep-screening live lemma to the three fields.
In the RS reading, shell multiplicity is recognition-energy occupancy; closing #132 is part of the geometric control on how many ordered pairs can sit on a single distance shell. The pack records what remains after the shared-endpoint diameter case is finished, so progress on thrackle support, diameter uniqueness, or deep-layer screening immediately upgrades the #132 claim without rewriting the final implication.
It does not touch the forcing chain (T5–T8) or the alpha residual band directly; those appear only as ambient RS context for why shell geometry is tracked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.