Erdos132OrderedConwayNoDeepResidualPack
plain-language theorem explainer
Packages two geometric hypotheses: the Conway straight-line thrackle support bound, and the pointwise ban on deep-layer structure in the low-shell diameter regime. Anyone reducing the ordered form of Erdős #132 to classical plane geometry cites this residual pack. It is a bare Prop structure with two fields; no proof body.
Claim. The ordered Conway / no-deep residual package 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 low-shell statement: if $\Delta$ is a diameter shell of $A$ with low-shell structure, then the deep-layer case does not occur.
background
The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, and shell multiplicity is occupancy. Ordered pairs are used for Lean bookkeeping; for positive distances the ordered multiplicity is twice the unordered one, so the classical bound $\le n$ becomes $\le 2n$.
The first field is the Conway thrackle support bound: if every pair of edges meets simply, the undirected support has at most $|A|$ edges (Lovász–Pach–Szegedy / Cairns–Nikolayevsky). The bound fails without the simple-meeting hypothesis (collinear overlaps).
The second field is the pointwise no-deep-layer statement in the low-shell regime: whenever $\Delta$ is a diameter shell carrying low-shell structure, the deep-layer case is forbidden. The Erdős target only needs an eventual form; the pointwise version is the cleaner classical geometry when finite exceptions are unnecessary.
proof idea
No proof: the declaration is a Prop-valued structure whose two fields are named hypotheses. Instantiating it means supplying proofs (or assumptions) of ConwayThrackleSupportBound and PointwiseNoDeepLayerCaseInLowShellRegime. Downstream, a one-line wrapper projects the two fields into the live reduction that yields the ordered Erdős #132 statement.
why it matters
This is the final residual package in the cleanest negative-layer form for the RS treatment of Erdős #132. The sole consumer is erdos132_from_ordered_conway_no_deep_residual_pack, whose doc-comment states that the ordered Conway plus pointwise no-deep residual package proves Erdős #132; it simply feeds the two fields into the live reduction erdos132_from_ordered_conway_and_pointwise_no_deep_layer_live.
In the broader Recognition framework the module treats distance multiplicity as recognition-energy shell occupancy. Closing this pack discharges the geometric residual that blocks the ordered #132 claim, separating thrackle counting from deep-layer screening so each can be attacked or cited independently.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.