DeepLayerCase
plain-language theorem explainer
Residual case class for a finite planar point set in the ordered-distance shell analysis of Erdős #132: every occupied shell other than a fixed diameter value fails to be sparse. Pair-budget pressure and convex-layer screening cite it as the obstruction that geometry must kill. It is a pure propositional structure (one universal field over the ordered spectrum), not a proved statement.
Claim. For a finite set $A\subset\mathbb{R}^2$ and a real $\Delta$, the deep-layer residual holds when every distance $r$ in the ordered pairwise distance spectrum of $A$ with $r\neq\Delta$ fails to be sparse, i.e. fails ordered shell multiplicity $\le 2|A|$.
background
This module is the Recognition Science physicalization of Erdős problem #132. Classically a distance value is a shell in the pairwise Euclidean spectrum; here it is a two-body recognition-energy shell whose occupancy is the multiplicity. The development works with ordered non-diagonal pair events on Point2 (the planar point type from the bipartite distance spectrum). For positive distances, ordered multiplicity is exactly twice the unordered count, so the classical sparse threshold $\le n$ becomes $\le 2n$.
A shell at radius $r$ is sparse when $r$ appears in the ordered spectrum and its ordered multiplicity is at most $2|A|$. The diameter shell is the unique maximum-distance shell. The deep-layer residual is the situation in which, relative to a chosen diameter value $\Delta$, every other occupied shell has not yet been certified sparse. The module doc frames this as the residual that later geometry bridges must rule out.
proof idea
Definitional structure, not a proved theorem. A single field packages the universal statement: for every spectrum radius $r\neq\Delta$, the sparse-shell predicate fails. The companion one-line lemma then applies the existing supercriticality criterion for non-sparse shells, yielding ordered multiplicity strictly above $2|A|$ on every such $r$. No tactic proof is attached to the structure itself.
why it matters
This is the residual obstruction left after finite shell accounting in the Erdős #132 plan. Downstream, the layer-flux alternative splits the low-shell regime into "second sparse shell exists" versus this residual. Pair-budget pressure uses it to force few occupied shells (each non-diameter shell eats at least $2|A|+1$ ordered events). Deep-layer screening and the convex-layer screen package both take the residual as hypothesis and demand a geometric contradiction (Clemen–Dumitrescu–Liu style layer data, or an explicit second sparse shell). The sharp global target is that in the low-shell regime the residual never occurs for large $|A|$. In RS language the shells are two-body recognition-energy levels; killing the residual closes the shell-flux bridge that feeds the broader distance-multiplicity program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.