erdos132_from_four_point_thrackle_and_no_deep_layer
plain-language theorem explainer
Assembles the ordered form of Erdős #132 from three geometric inputs: four-point diameter crossing, the undirected thrackle support bound, and no deep layer in the low-shell regime. Cited by anyone following the legacy thrackle route to two sparse distance shells on large planar sets. Proof is a short term reduction: convert the four-point hypothesis into endpoint-disjoint local meeting, then apply the core thrackle-plus-no-deep-layer assembly.
Claim. Assume: (i) any two endpoint-disjoint diameter pairs of length $\Delta$ in the plane, with all six pairwise distances $\le\Delta$, have intersecting closed segments; (ii) for all large $n$, any ordered edge set on an $n$-point planar set with no geometrically disjoint pair has undirected support of size at most $n$; (iii) for all large $n$, a diameter shell in the low-shell regime cannot be a deep-layer case. Then for every sufficiently large finite planar point set there exist two distinct sparse distance shells.
background
This 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 bookkeeping; for positive distances the ordered multiplicity is twice the unordered one, so the classical bound $\le n$ becomes $\le 2n$. The target Erdos132Ordered asserts that every large enough finite planar set carries two distinct sparse shells.
The three hypotheses are pure geometry. Four-point diameter crossing is the $n$-independent Hopf–Pannwitz core: endpoint-disjoint diameter segments whose cross-distances stay at most the diameter must meet. The undirected thrackle support bound is the Perles/Hopf–Pannwitz counting statement in set-theoretic form (at most $|A|$ undirected edges when no pair is geometrically disjoint). No-deep-layer in the low-shell regime is the residual contradiction left after finite shell accounting: a diameter shell that already has low-shell structure cannot still be a deep layer.
Doc-comment flags this assembly as legacy: the four-point geometry is live, but the support bound permits overlapping collinear segments and is not the final global count (Conway is used downstream).
proof idea
Term-mode one-step reduction. First apply endpoint_disjoint_local_meeting_from_four_point to the four-point diameter crossing hypothesis, obtaining the endpoint-disjoint local-meeting form required by the core lemma. Then invoke erdos132_from_endpoint_disjoint_diameter_core_thrackle_and_no_deep_layer on that converted hypothesis together with the undirected thrackle support bound and the no-deep-layer hypothesis. No further case analysis or arithmetic is performed here.
why it matters
Sits on the legacy thrackle path toward the RS reading of Erdős #132 (two sparse recognition-energy shells on large planar sets). The sole recorded consumer is erdos132_from_four_point_thrackle_and_convex_layer_screening, which replaces the no-deep-layer input by a convex-layer screening bridge and still routes through this theorem. The module doc frames the whole development as the physicalization of distance-shell multiplicity; this declaration packages the four-point geometry with the deprecated set-theoretic support bound before the Conway correction. It does not touch the forcing chain (T0–T8) or the RCL directly; its role is combinatorial geometry feeding the shell-occupancy story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.