Erdos132ConwayCountingScreeningResidualPack
plain-language theorem explainer
Packages the two residual hypotheses still needed for the ordered Erdős #132 statement: a support-level Conway straight-line thrackle bound, and a pointwise deep-layer screening certificate on diameter shells. Anyone citing the live residual route to ordered shell multiplicity will use this pack. It is a pure Prop structure with no proof body; the companion theorem unpacks the fields.
Claim. A residual package for ordered Erdős problem #132 is a pair of assertions: (i) for every finite point set $A\subset\mathbb{R}^2$ and every ordered edge set $E$ supported on $A$ that forms a Conway thrackle support, the unordered edge support of $E$ has cardinality at most $|A|$; (ii) for every finite $A$ and diameter shell value $\Delta$, if $A$ has low-shell structure at $\Delta$ then deep-layer screening holds at $(A,\Delta)$.
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 shell multiplicity. Ordered pairs are used for Lean simplicity, so the classical bound $\le n$ becomes $\le 2n$ on ordered multiplicity.
ConwayThrackleSupportBoundOnSupport is the support-level thrackle bound suited to ordered finsets that may carry both orientations of an undirected edge: any Conway thrackle support $E$ on $A$ satisfies $|\mathrm{unorderedEdgeSupport}(E)|\le|A|$. PointwiseDeepLayerScreeningCertificate is the pointwise positive form of the layer residual: under a diameter shell $\Delta$ and low-shell structure, deep-layer screening holds, which forces a second sparse shell and rules out the residual deep-layer case.
The pack is the live residual interface after the full diameter-side Conway condition was closed. The signed $\alpha$-genesis residual appears only as an ambient RS constant dependency, not as a geometric hypothesis here.
proof idea
No proof body: the declaration is a two-field structure ... : Prop. Inhabitation is by supplying proofs of the support-level Conway thrackle bound and of the pointwise deep-layer screening certificate. The companion theorem erdos132_from_conway_counting_screening_residual_pack is a one-line unpack that feeds both fields into erdos132_from_support_conway_and_deep_screening_live to obtain the ordered Erdős #132 statement.
why it matters
This is the current residual package for the RS physicalization of Erdős #132 after diameter-side Conway work closed. Downstream, erdos132_from_conway_counting_screening_residual_pack converts any inhabitant of the pack into Erdos132Ordered, the ordered form of the distinct-distance shell bound (multiplicity $\le 2n$).
In the Recognition reading, sparse shells and diameter shells are recognition-energy layers; thrackle counting and deep-layer screening are the combinatorial controls that force a second sparse shell when the low-shell hypotheses hold. The pack therefore marks exactly which two geometric certificates remain between the closed Conway diameter side and a full ordered proof of #132. It does not itself settle the classical problem; it freezes the residual interface the companion theorem consumes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.