Erdos132CurrentLiveResidual
plain-language theorem explainer
Packages the two remaining geometric inputs for the ordered Erdős #132 theorem: the Conway straight-line thrackle support bound and the global convex-layer screening bridge. Anyone assembling the ordered multiplicity bound cites this residual as the live endpoint. Pure definitional conjunction; no proof content.
Claim. The current live residual for Erdős problem #132 is the conjunction of two statements: (i) if $E$ is a Conway thrackle on a finite point set $A\subset\mathbb{R}^2$ (every pair of edges meets simply), then the undirected edge support of $E$ has size at most $|A|$; (ii) for all sufficiently large finite $A\subset\mathbb{R}^2$ and every diameter shell $\Delta$ of $A$, first/second convex-layer data screen the low-shell residual deep-layer case.
background
The module physicalizes Erdős #132 inside Recognition Science: a classical distance value is a two-body recognition-energy shell, and its multiplicity is shell occupancy. Lean works with ordered pairs, so the classical unordered bound $\le n$ becomes the ordered threshold $\le 2n$.
Upstream, the Conway thrackle support bound is the Lovász–Pach–Szegedy / Cairns–Nikolayevsky counting theorem: under the simple-meeting hypothesis, undirected support size is at most $|A|$ (false without that hypothesis, by collinear overlaps). The convex-layer screening bridge is the remaining layer-flux statement: every large enough finite set admits first/second layer data that kill the residual deep-layer case in the low-shell regime.
Doc-comment status: all finite accounting, diameter geometry, ordered/unordered bookkeeping, and the support-level Conway correction are already discharged above this residual.
proof idea
Definitional packaging only. The residual is the propositional conjunction of ConwayThrackleSupportBound and ConvexLayerScreeningBridge. No tactics, no lemmas applied at this site.
why it matters
This is the live two-input endpoint named by the proof plan for the RS treatment of Erdős #132. Downstream, erdos132_from_current_live_residual consumes exactly this residual and returns the ordered theorem Erdos132Ordered by feeding the two conjuncts into the ordered Conway-plus-convex-layer assembly. A parallel final-components path (erdos132_from_final_components) packages Hopf–Pannwitz diameter sparsity with a no-deep-layer hypothesis instead; the present residual is the currently preferred live cut.
In the broader framework the module records a physicalization, not a forcing-chain step: distance shells are two-body recognition-energy shells, so the classical multiplicity bound becomes a statement about shell occupancy. Closing either conjunct (thrackle support or convex-layer screening) would discharge this residual and finish the ordered theorem along the live path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.