Erdos132CurrentLargeNonStarResidual
plain-language theorem explainer
Packages the two remaining open hypotheses for the ordered form of Erdős problem #132: the large non-star Conway thrackle support bound, and the global convex-layer screening bridge. Small and star Conway cases are treated as already closed by finite bookkeeping, so only this large non-star residual remains on the counting side. Citation target for the live residual path to #132. Pure definitional conjunction of those two propositions.
Claim. The current large non-star residual is the conjunction of (i) the large non-star residual form of Conway's straight-line thrackle support bound (ambient sets of size at least $4$, stars already excluded) and (ii) the global convex-layer screening theorem: every sufficiently large finite planar point set admits first/second layer data that screens the low-shell residual deep-layer case on a diameter shell.
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 conjunct is the large non-star residual form of Conway's straight-line thrackle theorem: star systems and ambient sets with $|A|\le 3$ are finite bookkeeping, leaving the first genuinely large Conway counting target. The second conjunct is the global convex-layer screening theorem named by the plan: every sufficiently large finite set admits first/second layer data that screens the low-shell residual deep-layer case on a diameter shell.
An upstream residual constant from the alpha-genesis stack (signed gap of the first-order inverse-alpha against CODATA) is referenced in the dependency graph but is not part of the proposition body itself.
proof idea
Definitional abbreviation only: the proposition is the logical conjunction of the large non-star Conway thrackle support bound and the convex-layer screening bridge. No tactics, no lemmas applied, no reduction. Downstream theorems unpack the pair as .1 and .2 and feed them into the ordered Conway-plus-screening assembly.
why it matters
This is the live residual interface for the RS treatment of Erdős #132. The immediate parent is the theorem that, given this residual, concludes the ordered form of #132: it converts the large non-star Conway conjunct into a full Conway support bound (small and star cases already bookkept) and pairs that with the convex-layer screening bridge.
In the module's forcing narrative, distance shells are recognition-energy shells; closing multiplicity bounds is the combinatorial half of the physicalization. The residual deliberately isolates what remains after finite casework: large non-star thrackle counting plus layer-flux screening. It does not itself touch the T0–T8 chain, RCL, or the alpha band, but it is the mathematics-side bottleneck named by the current plan for #132.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.