Erdos132ConwayEndpointDisjointCollinearityScreeningResidualPack
plain-language theorem explainer
Packages the three residual hypotheses that finish the ordered form of Erdős problem #132: a support-level Conway thrackle bound, the two-point collinearity certificate for endpoint-disjoint diameter edges, and pointwise deep-layer screening. Anyone citing the residual route to the ordered multiplicity bound would use this pack. It is a pure Prop structure with no proof body; the downstream theorem just projects the three fields.
Claim. A residual package asserting three statements: (i) every Conway thrackle support $E$ on a finite point set $A$ has unordered edge-support cardinality at most $|A|$; (ii) if two endpoint-disjoint diameter representatives of a diameter shell $\Delta$ share two distinct common points, then the second representative's endpoints lie on the line through the first; (iii) under low-shell structure on a diameter shell, deep-layer screening holds pointwise (any residual deep-layer case produces a second sparse shell).
background
The module physicalizes Erdős problem #132 inside Recognition Science: a classical distance value is a two-body recognition-energy shell, and its multiplicity is shell occupancy. Ordered pairs are used for Lean simplicity; for positive distances the ordered multiplicity is twice the unordered one, so the classical bound $\le n$ becomes $\le 2n$.
The three fields are the live residual surface after endpoint-disjoint uniqueness was reduced to a two-point collinearity certificate. The thrackle field is the support-level Conway bound (unordered edge support of a thrackle on $A$ has size $\le |A|$), correct for ordered finsets that may carry both orientations. The collinearity field is pure affine incidence: two distinct common points force both endpoint-disjoint diameter representatives onto one line. The screening field is the pointwise Deep-Layer Screening Lemma: under low-shell hypotheses any residual deep-layer case yields the missing second sparse shell.
Upstream, the collinearity Prop is already discharged by an affine-incidence theorem; the pack simply names that certificate alongside the thrackle and screening surfaces.
proof idea
No proof body: this is a structure of type Prop whose three fields are named residual hypotheses. Instantiating it means supplying proofs (or prior theorems) of the support-level Conway thrackle bound, the endpoint-disjoint two-point collinearity certificate, and the pointwise deep-layer screening certificate. Downstream consumption is a one-line projection into the existing combiner that turns those three surfaces into the ordered Erdős #132 statement.
why it matters
This is the current live residual package for the RS physicalization of Erdős #132. The sole downstream consumer is the theorem that, given any instance of the pack, concludes the ordered form of the problem (ordered shell multiplicity $\le 2n$). That theorem simply feeds the three fields into the already-assembled combiner for support Conway thrackle, endpoint-disjoint collinearity, and deep-layer screening.
In the module's terms, the classical distance-shell multiplicity bound is rephrased as a recognition-energy shell occupancy bound. Closing this pack therefore closes the ordered route to #132 inside the Distance Shell Multiplicity development. It does not itself touch the forcing chain (T0–T8) or the RCL; it is pure discrete geometry serving the RS reading of the Erdős problem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.