layer_flux_alternative_of_definitions
plain-language theorem explainer
For any finite planar point set and diameter threshold, either a second sparse distance shell exists after the diameter is removed, or the configuration is residual deep-layer. Packers of shell-flux components for the Erdős #132 physicalization cite this split. The argument is a classical case distinction that unfolds the two sides of the alternative from their definitions; no geometry is used.
Claim. For every finite set $A$ of points in the Euclidean plane and every real $\Delta$, either there exists a radius $r \neq \Delta$ at which $A$ has a sparse distance shell, or the residual deep-layer case holds for $(A,\Delta)$.
background
The module physicalizes Erdős problem #132. Classically a distance value is a shell in the pairwise Euclidean spectrum; physically it is a two-body recognition-energy shell whose multiplicity is occupancy. Ordered pairs are used for Lean simplicity: for a positive distance, ordered multiplicity is twice the unordered count, so the classical threshold $\le n$ becomes $\le 2n$.
Points live in the Euclidean plane (Point2). A sparse shell is a distance whose ordered multiplicity is low. The diameter shell is the unique maximal-distance shell. Existence of a second sparse shell means some radius $r \neq \Delta$ is sparse. The deep-layer case is the residual obstruction: no non-diameter occupied shell has yet been shown sparse (upstream: "the later geometry bridge must rule these cases out").
The layer-flux alternative is the Prop structure whose single field is the disjunction of those two situations.
proof idea
Classical case split on existence of a second sparse shell. On the positive branch, inject the left disjunct into the alternative structure. On the negative branch, the negation is definitionally the deep-layer residual: any candidate radius that is occupied, unequal to $\Delta$, and sparse would witness a second sparse shell, contradiction. Populate the right disjunct and close. Pure definitional unfolding of the alternative and of the residual case; no geometric lemma is invoked.
why it matters
Downstream, shell_flux_component_pack_of_reduced lifts a reduced shell-flux package to the full component package "by the definitional layer-flux split." The local doc-comment is explicit that the hard geometry is not this split but screening the residual deep-layer case. In the RS reading of Erdős #132, sparse shells control recognition-energy occupancy; the alternative isolates the remaining obstruction that later geometry bridges must eliminate. No T0–T8 forcing step, RCL identity, or constant band is touched; this is combinatorial scaffolding inside the distance-shell multiplicity development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.