Erdos132OrderedConwayConvexLayerResidualPack
plain-language theorem explainer
A residual hypothesis package for the ordered form of Erdős problem #132: it bundles the Conway straight-line thrackle support bound with the global convex-layer screening bridge. Anyone citing the ordered-pair reduction of #132 uses this pack as the final component interface. As a Prop structure it carries no proof body; discharge is by supplying both component hypotheses.
Claim. A residual package asserting two propositions: (i) every finite straight-line Conway thrackle on a point set $A$ has undirected edge support of size at most $|A|$; (ii) for all sufficiently large finite $A\subset\mathbb{R}^2$, and every diameter shell $\Delta$, there exist first/second convex-layer data that screen the low-shell residual deep-layer case.
background
The module physicalizes Erdős problem #132 in Recognition Science language: a classical distance value is a shell in the pairwise Euclidean spectrum; physically it is a two-body recognition-energy shell whose multiplicity is shell occupancy. Ordered pairs are used for Lean simplicity, so the classical multiplicity threshold $\le n$ becomes $\le 2n$ for positive distances.
The first component 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 component is the global convex-layer screening bridge: every sufficiently large finite set admits first/second layer data that screens the low-shell residual deep-layer case. That is the remaining layer-flux theorem named by the proof plan.
proof idea
No proof body: the declaration is a Prop-valued structure with two fields. It simply records simultaneous assumption of the Conway thrackle support bound and the convex-layer screening bridge. Downstream, the one-line theorem erdos132_from_ordered_conway_convex_layer_residual_pack unpacks the two fields and feeds them to the live combiner that yields the ordered Erdős #132 statement.
why it matters
This is the final residual package in the proof plan's component language for the ordered form of Erdős #132. The sole direct consumer is the theorem that, given any such pack, concludes the ordered Erdős #132 claim by applying the live Conway-plus-screening combiner. In the RS reading, closing #132 controls distance-shell multiplicities (two-body recognition-energy shells). The pack isolates exactly the two remaining geometric inputs: thrackle counting on ordered supports and convex-layer flux screening of deep residual shells. It does not itself settle either input; it names the interface that, once both are proved, finishes the ordered reduction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.