ShellFluxComponentPack
plain-language theorem explainer
Packages four asymptotic bridge targets that together close the shell-flux argument for ordered Erdős #132 on planar point sets. Anyone citing the component-based route to a second sparse distance shell uses this bundle. It is a pure Prop structure: each field is a classical finite-geometry claim about diameter shells, pair budgets, layer flux, and deep-layer screening; no proof body.
Claim. A shell-flux component package is a proposition asserting four eventual statements for finite planar sets $A$ of size $n\to\infty$ and diameter distance $\Delta$: (i) every diameter shell satisfies pair-budget pressure; (ii) diameter plus pair-budget pressure yields the low-shell regime (at most $|A|/2+2$ occupied shells); (iii) diameter plus low-shell structure yields the layer-flux alternative (a second sparse shell exists, or a deep-layer residual case); (iv) diameter plus low-shell structure yields deep-layer screening (every deep-layer residual forces a second sparse shell).
background
The module physicalizes Erdős problem #132: a distance value is a shell in the pairwise Euclidean spectrum; multiplicity is shell occupancy. Ordered pairs are used for Lean simplicity, so the classical bound $\le n$ becomes $\le 2n$ for positive distances.
A diameter shell is the maximum value in the ordered distance spectrum of a finite planar set $A\subset\mathbb{R}^2$. Pair-budget pressure says that in a deep-layer residual case the occupied-shell count is forced into the low-shell regime ($\le |A|/2+2$). Low-shell structure is exactly that cardinality bound. The layer-flux alternative is the split "second sparse shell or deep-layer case"; deep-layer screening asserts the residual case cannot persist and must produce a second sparse shell.
Together these four fields are the standalone classical bridge targets named by the proof plan for the shell-flux bridge.
proof idea
No proof: this is a structure of type Prop whose four fields are named asymptotic hypotheses. Construction of an instance is deferred. The reduced package (after noting that the layer-flux alternative is definitionally the exit-or-residual split) supplies a full package via shell_flux_component_pack_of_reduced. Downstream, second_sparse_shell_flux_bridge_from_components assembles the four fields with filter_upwards into the missing shell-flux bridge.
why it matters
This is the executable interface between the HTML proof plan and the ordered form of Erdős #132. Parent theorem second_sparse_shell_flux_bridge_from_components states that the package closes the missing shell-flux bridge; erdos132_from_hopf_pannwitz_and_components then combines Hopf–Pannwitz with that bridge to obtain Erdos132Ordered.
In Recognition Science terms the module treats distance shells as two-body recognition-energy shells. The component split isolates pure finite accounting (pair budget) from convex-layer geometry (screening), so each classical target can be attacked independently. The reduced package is the sharper implementation target once the layer-flux alternative is recognized as tautological.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.