shell_flux_component_pack_of_reduced
plain-language theorem explainer
Any reduced shell-flux component package upgrades to a full component package: the two missing fields are pure counting and a definitional case split. Combinatorialists working the RS form of Erdős #132 cite this to feed the final assembly from Hopf–Pannwitz plus reduced components. The proof is a short field-wise construction applying two local lemmas and copying the hard geometric fields.
Claim. If $C$ is a reduced shell-flux component package (asymptotic low-shell structure and deep-layer screening on diameter shells), then there exists a full shell-flux component package: pair-budget pressure, low-shell structure, the layer-flux alternative, and deep-layer screening all hold for all sufficiently large finite point sets $A\subset\mathbb{R}^2$ and diameter distances $\Delta$.
background
The module physicalizes Erdős problem #132: a distance value is a two-body recognition-energy shell, and ordered multiplicity is twice the classical unordered count, so the classical bound $\le n$ becomes $\le 2n$.
A full shell-flux component package bundles four asymptotic bridges on diameter shells of an $n$-point set in the plane: pair-budget pressure (few occupied shells in the deep residual case), low-shell structure, a layer-flux alternative (second sparse shell versus residual deep layer), and deep-layer screening. The reduced package drops the first and third fields after observing they are not geometric.
Upstream, pair_budget_pressure_from_counting is pure finite accounting: in a deep residual case every non-diameter shell is supercritical, so at most $|A|/2$ of them exist. Separately, layer_flux_alternative_of_definitions is the tautology "either a second sparse shell exists, or we are residual"; the hard geometry is screening the residual case.
proof idea
Construct the four fields of the full package from the reduced package $C$.
For pair-budget pressure, filter eventually in $n$, take a diameter shell $\Delta$ on an $n$-set $A$, and apply pair_budget_pressure_from_counting.
Copy low_shell_structure and deep_layer_screening verbatim from $C$.
For the layer-flux alternative, filter eventually in $n$ and apply layer_flux_alternative_of_definitions, which splits on existence of a second sparse shell by definition.
No new geometric argument appears; the reduced package already carries the hard fields.
why it matters
This is the definitional bridge from the sharper implementation target (reduced components) to the full component package demanded by the shell-flux proof plan. Downstream, erdos132_from_hopf_pannwitz_and_reduced_components applies it once: given Hopf–Pannwitz on ordered diameters and a reduced package $C$, it builds the full package via this theorem and feeds erdos132_from_hopf_pannwitz_and_components, closing the ordered Erdős #132 statement.
In the RS reading, shell occupancy is recognition-energy multiplicity on two-body distance shells. Closing the component package is the last combinatorial step before the physicalized #132 claim. The theorem itself does not touch the forcing chain (T0–T8) or the mass ladder; it is pure discrete geometry scaffolding inside the distance-shell module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.