ShellFluxMinimalGeometryPack
plain-language theorem explainer
Packages the single remaining geometric hypothesis after finite pair-budget accounting for the ordered-pair form of Erdős #132: for all large n, every planar n-point set whose diameter shell is already in the low-shell regime admits deep-layer screening. Cited by anyone closing the shell-flux bridge or the full ordered Erdős #132 theorem from Hopf–Pannwitz. It is a one-field Prop structure, not a proved statement.
Claim. A property asserting that eventually, for every finite planar point set $A$ with $|A|=n$ and every diameter value $\Delta$ of $A$, if $A$ has low-shell structure (occupied distance-shell count at most $|A|/2+2$), then deep-layer screening holds: any residual deep-layer case for $(A,\Delta)$ forces the existence of a second sparse shell.
background
This module physicalizes Erdős problem #132: a classical distance value is a shell in the pairwise Euclidean spectrum; in RS it is a two-body recognition-energy shell, and multiplicity is shell occupancy. Ordered pairs are used for Lean simplicity, so the classical bound $\le n$ becomes $\le 2n$.
Point2 is the planar point type. A diameter shell is a value $\Delta$ in the ordered distance spectrum that is maximal among all realized distances. Low-shell structure means the configuration has entered the small radial spectrum regime: the number of occupied shells is at most $|A|/2+2$, where convex-layer analysis must take over. Deep-layer screening is the residual obstruction package: if a deep-layer case occurs, a second sparse shell already exists.
After finite pair-budget pressure is implemented, the only nontrivial geometric work left is screening that residual deep-layer case once the low-shell bound is in hand.
proof idea
No proof body: this is a Prop-valued structure definition with a single field. That field packages the filter statement "for all sufficiently large $n$, every $n$-point planar set whose diameter shell satisfies low-shell structure also satisfies deep-layer screening." Downstream constructors (e.g. from a global no-deep-layer hypothesis) and consumers simply inhabit or project this field; there is no algebraic reduction here.
why it matters
This is the minimal remaining geometry package in the shell-flux route to ordered Erdős #132. The parent theorem second_sparse_shell_flux_bridge_from_minimal_geometry turns the pack into the full shell-flux bridge by splitting on whether a second sparse shell already exists or the residual deep-layer case must be screened under the low-shell hypothesis supplied by finite counting. That bridge, together with Hopf–Pannwitz, yields erdos132_from_hopf_pannwitz_and_minimal_geometry.
A separate constructor shows that a global "no deep-layer case in the low-shell regime" hypothesis is exactly enough to inhabit the pack. In the RS reading, distance shells are recognition-energy shells; closing this geometric residue is what lets the classical multiplicity bound land as a physical shell-occupancy statement. The pack isolates the sharp geometric theorem left after all finite accounting reductions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.