Erdos132OrderedConwayThresholdLayerResidualPack
plain-language theorem explainer
Residual hypothesis pack for the ordered form of Erdős #132: the Conway straight-line thrackle support bound together with a thresholded convex-layer screening certificate. Anyone discharging the RS physicalization of #132 cites this bundle. Pure Prop structure with empty body; the consumer theorem unpacks the two fields and applies the live bridge.
Claim. The residual package asserting both (i) the Conway straight-line thrackle support bound: every finite point set $A$ and every simple thrackle $E$ on $A$ has undirected edge support of cardinality at most $|A|$; and (ii) a thresholded convex-layer screening certificate: there exists a finite $N$ such that every configuration with at least $N$ points, for any diameter shell $\Delta$, admits first/second convex-layer data that screens the low-shell residual deep-layer case.
background
The module physicalizes Erdős problem #132 in Recognition Science language. Classically a distance value is a shell in the pairwise Euclidean spectrum; here it is a two-body recognition-energy shell whose multiplicity is shell occupancy. Ordered pairs are used for Lean simplicity: for positive distances, ordered multiplicity is twice the unordered count, so the classical bound $\le n$ becomes $\le 2n$.
The first field is the Conway straight-line thrackle support bound (Lovász–Pach–Szegedy / Cairns–Nikolayevsky): if every pair of edges meets simply, the undirected support has size at most $|A|$. The bound fails without the simple-meeting hypothesis (collinear overlaps).
The second field is the most concrete remaining layer statement: exhibit finite $N$ so that every large enough point set has first/second convex-layer data screening the low-shell residual deep-layer case on any diameter shell.
proof idea
No proof body: this is a Prop-valued structure that merely packages two named residual hypotheses as fields. Downstream consumers project the fields and feed them to the live bridge that turns ordered Conway counting plus thresholded convex-layer screening into the ordered Erdős #132 statement. Construction is by supplying witnesses for each field Prop.
why it matters
This is the final residual package with an explicit convex-layer threshold for the ordered #132 route. Its sole consumer is the theorem that, given the pack, concludes the ordered Erdős #132 claim by applying the live bridge to the two projected fields. In the module's RS reading, closing those two residuals finishes the physicalization of #132 (distance shells as two-body recognition-energy shells with controlled occupancy). It does not itself touch the forcing chain T0–T8; it sits in the combinatorial mathematics layer that the monolith uses to encode classical distance problems in recognition language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.