ShellFluxReducedComponentPack
plain-language theorem explainer
A two-field Prop packaging the reduced shell-flux bridge for the ordered Erdős #132 program: asymptotically, diameter shells under pair-budget pressure enter the low-shell regime, and once there, deep-layer residuals are screened to a second sparse shell. Anyone assembling the hopf–pannwitz-plus-components route cites this as the sharper proof target. It is a pure interface definition; no proof body.
Claim. A reduced shell-flux component package is the conjunction of two asymptotic statements for finite planar point sets $A$ of size $n\to\infty$ and diameter distance $\Delta$: (i) pair-budget pressure on the diameter shell implies low-shell structure (occupied shell count $\le |A|/2+2$); (ii) low-shell structure on the diameter shell implies deep-layer screening (every deep-layer residual yields a second sparse shell).
background
The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, with ordered-pair multiplicity twice the unordered count, so the classical bound $\le n$ becomes $\le 2n$. Points live in the Euclidean plane (Point2). A diameter shell is a value in the ordered distance spectrum that is maximal among all realized distances.
Pair-budget pressure is finite accounting: in a deep-layer residual, non-diameter shells are supercritical, so at most $|A|/2$ of them exist and occupied shells are at most $|A|/2+2$. Low-shell structure is exactly that occupancy bound, the regime where convex-layer geometry takes over. Deep-layer screening asserts that residual deep-layer cases cannot persist: they force a second sparse shell.
The older layer-flux alternative (second sparse shell or deep-layer case) is definitional once low-shell structure holds. The reduced package therefore drops that tautology and keeps only the two nontrivial bridges: pressure $\Rightarrow$ low shells, and low shells $\Rightarrow$ screening.
proof idea
No proof: this is a structure of propositions, not a theorem. It names the two asymptotic fields that a later construction must inhabit. Downstream, shell_flux_component_pack_of_reduced rebuilds the full component package by inserting the definitional layer-flux split, then erdos132_from_hopf_pannwitz_and_reduced_components feeds the result into the hopf–pannwitz assembly.
why it matters
This is the sharpened implementation target for the remaining classical geometry in the ordered Erdős #132 bridge. The module frames distance multiplicity as recognition-energy shell occupancy; closing the shell-flux path is what turns hopf–pannwitz diameter control into the full ordered statement.
Parents: shell_flux_component_pack_of_reduced lifts this reduced pack to the full component pack via the definitional exit-or-residual split; erdos132_from_hopf_pannwitz_and_reduced_components is the final assembly theorem that takes hopf–pannwitz plus this pack and concludes the ordered Erdős claim. By stripping the tautological layer-flux field, the structure isolates exactly the two geometric obligations still owed by the proof plan.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.