PointwiseDeepLayerScreeningCertificate
plain-language theorem explainer
The pointwise deep-layer screening certificate is the Prop that every finite planar point set with a diameter shell and low-shell structure satisfies deep-layer screening. It is the packaged Deep-Layer Screening Lemma from the Erdős #132 residual plan. Anyone assembling ordered or support-level residual packs for the RS form of #132 cites it as one of two live inputs beside Conway thrackle support bounds. As a definitional Prop it has no proof body beyond the quantified statement.
Claim. For every finite $A \subset \mathbb{R}^2$ and every $\Delta \in \mathbb{R}$, if $\Delta$ is a diameter shell of $A$ and $A$ has low-shell structure at $\Delta$, then deep-layer screening holds for $(A,\Delta)$.
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, ordered multiplicity is twice the unordered count, so the classical bound $\le n$ becomes $\le 2n$.
Points live in $\mathbb{R}^2$ (the bipartite spectrum's Point2). A diameter shell is a distance shell realizing the set diameter. Low-shell structure packages the local sparse-shell hypotheses on that diameter. Deep-layer screening is the positive statement that rules out the residual deep-layer case: by definition that residual case asserts there is no second sparse shell, so screening forces the missing second sparse shell under the low-shell hypotheses.
Upstream geometry is ordinary Euclidean distance on finite planar sets; the certificate does not itself invoke RS constants, only the combinatorial shell language of the module.
proof idea
Definitional Prop, not a proved theorem. The body is a triple universal quantifier over finite planar point sets $A$ and reals $\Delta$, with two hypotheses (diameter shell, low-shell structure) implying deep-layer screening. No tactics, no lemmas applied: it simply names the Deep-Layer Screening Lemma in pointwise form so residual packs can take it as a single hypothesis.
why it matters
This certificate is one of the two remaining live inputs in every current residual package for the ordered Erdős #132 claim. Downstream structures (Erdos132ConwayCountingScreeningResidualPack, the endpoint-disjoint uniqueness and collinearity packs, and the ordered Conway pack) each carry a field requiring it beside a Conway thrackle support bound. Live assembly theorems such as erdos132_from_support_conway_and_deep_screening_live and erdos132_from_ordered_conway_and_deep_screening_live take the certificate as an explicit hypothesis and discharge Erdos132Ordered.
In the proof plan it is exactly the Deep-Layer Screening Lemma: under low-shell hypotheses any residual deep-layer case produces the missing second sparse shell. Closing it (together with Conway counting) finishes the RS physicalization of #132 in this module. It does not touch the forcing chain T0–T8 or the RCL; it is pure planar distance-shell combinatorics feeding the multiplicity bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.