ConvexLayerData
plain-language theorem explainer
Abstract first/second convex-layer package on a finite planar point set: two subsets of the ambient set, with no geometric construction forced yet. Downstream shell-flux and screening statements cite it as the local data type for a Clemen–Dumitrescu–Liu style bridge. It is a pure structure definition, so there is no proof body.
Claim. For a finite planar point set $A$, a convex-layer data package is a pair of subsets $L_1,L_2\subseteq A$ (intended as the first and second convex layers). No further geometric axioms are required at this stage.
background
The module physicalizes Erdős problem #132 inside Recognition Science: 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. Ordered pairs are used for Lean simplicity, so for a positive distance the ordered multiplicity is twice the unordered one and the classical bound $\le n$ becomes $\le 2n$.
Points are planar (Point2 from the bipartite distance-spectrum setup). Diameter shells and low-shell / deep-layer case distinctions appear later in the same module; this structure only packages the two layer sets that those arguments will consume.
The design is deliberately thin: geometric construction of convex layers can be filled in later, while the shell-flux proofs already know which subset data they need.
proof idea
No proof. The declaration is a structure with four fields: two finite subsets of the ambient planar set and the two subset proofs. Downstream predicates (e.g. the local screening predicate) take an instance of this package as a parameter and state what those layers must achieve.
why it matters
This is the local data carrier for the Clemen–Dumitrescu–Liu style convex-layer bridge named in the plan. The local screening predicate asserts that a package is strong enough to kill the residual deep-layer case on one chosen diameter shell. The global bridge and its thresholded certificate quantify over large finite sets and demand existence of such packages. A short implication theorem then turns the global bridge into the no-deep-layer target in the low-shell regime.
In the RS reading of Erdős #132, closing that residual deep-layer case is the remaining layer-flux step: without a typed layer package, the screening statements have nothing to quantify over. The structure therefore sits between pure combinatorial geometry and the physical shell-multiplicity claims of the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.