LayerFluxAlternative
plain-language theorem explainer
For a finite planar point set and a distinguished diameter distance Δ, either a second sparse distance shell exists besides the diameter shell, or every remaining occupied shell is still supercritical (the deep-layer residual). Anyone working the RS reading of Erdős #132 cites this as the case split that isolates the hard geometry. It is a pure Prop structure: a named disjunction of two already-defined predicates, with no proof content of its own.
Claim. For a finite set $A$ of planar points and a real distance $\Delta$, the layer-flux alternative holds when either there exists a second sparse shell at some distance $r \neq \Delta$, or $A$ is in the deep-layer residual case: every occupied non-diameter shell fails to be sparse.
background
The module physicalizes Erdős problem #132 inside Recognition Science. Classically a distance value is a shell in the pairwise Euclidean spectrum; here it is a two-body recognition-energy shell whose multiplicity is shell occupancy. The development works with ordered pairs, so for a positive distance the ordered multiplicity is twice the unordered one and the classical bound $\le n$ becomes $\le 2n$.
Point2 is the planar point type from the bipartite distance spectrum. A sparse shell at radius $r$ is the desired low-occupancy shell. ExistsSecondSparseShell A Δ asserts some $r \neq \Delta$ that is sparse. DeepLayerCase A Δ is the complementary residual: every occupied non-diameter shell in the ordered spectrum has not yet been shown sparse (equivalently, each such shell is supercritical). The diameter shell itself is handled separately by uniqueness and nonnegativity lemmas earlier in the file.
proof idea
No proof body: this is a structure-as-Prop packaging a single field, the disjunction of the two predicates already defined above. The companion theorem layer_flux_alternative_of_definitions discharges the structure by classical case split on whether a second sparse shell exists, injecting the left or right disjunct. The structure itself contributes only the named interface.
why it matters
This is the bookkeeping hinge in the shell-flux bridge for the RS form of Erdős #132. Downstream, layer_flux_alternative_of_definitions shows the split is tautological at the level of current definitions, so the real work is screening the deep-layer residual. ShellFluxComponentPack packages the classical bridge targets (pair-budget pressure, low-shell structure, and related components); second_sparse_shell_flux_bridge_from_components then closes the missing shell-flux bridge from that pack. In framework terms the multiplicity counts are recognition-energy shell occupancies on planar configurations, feeding the distance-spectrum side of the mathematics layer rather than the T0–T8 forcing chain directly. The open geometric obligation is ruling out deep-layer cases so that a second sparse shell is forced in the low-shell regime.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.