Erdos132CurrentConstructiveResidual
plain-language theorem explainer
Packages the live constructive residual for Erdős #132 as the conjunction of a Conway straight-line thrackle endpoint-charge certificate and a global convex-layer screening bridge. Anyone citing the constructive route to the ordered shell-multiplicity bound uses this Prop. It is a pure definitional abbreviation with no proof obligations of its own.
Claim. The current constructive residual is the proposition that both of the following hold: (i) every finite straight-line Conway thrackle admits an injective endpoint charge of its unordered edges onto ambient vertices; (ii) for all sufficiently large finite planar point sets, first/second convex-layer data screen the low-shell residual in the deep-layer case (relative to a diameter shell).
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, and its multiplicity is shell occupancy. Lean works with ordered pairs, so for positive distances ordered multiplicity is twice the unordered count and the classical bound $\le n$ becomes $\le 2n$.
The first conjunct is the constructive Conway thrackle target: for each finite straight-line Conway thrackle on a point set, charge each unordered edge injectively to one ambient vertex. That form is cardinality-equivalent to the classical thrackle bound and is the intended formalization target.
The second conjunct is the global convex-layer screening bridge: every sufficiently large finite set admits first/second-layer data that screen the low-shell residual deep-layer case whenever a diameter shell is fixed. Together they are the named remaining layer-flux package for the constructive path.
proof idea
Definitional, not a proof. The body is the propositional conjunction of ConwayThrackleEndpointChargeCertificate and ConvexLayerScreeningBridge. No tactics, no lemmas applied, no sorry. Downstream theorems treat an assumption of this Prop as a pair of hypotheses and project the two conjuncts.
why it matters
This is the single named residual that the constructive discharge theorem consumes. The immediate parent is erdos132_from_current_constructive_residual, whose doc-comment states that the constructive current residual proves Erdős #132: from the residual it derives the ordered Conway support bound from the endpoint-charge certificate, then feeds that bound plus the convex-layer screening bridge into the live ordered Conway-and-screening lemma to obtain Erdos132Ordered.
In the module's RS reading, closing this residual is the constructive route to the ordered shell-multiplicity statement (classical $\le n$, ordered $\le 2n$). It does not itself touch the forcing chain T0–T8 or the RCL; it sits in the mathematics layer that physicalizes distance shells as recognition-energy shells. The open work is proving each conjunct, not rearranging this package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.