SecondSparseShellFluxBridge
plain-language theorem explainer
Names the missing shell-flux bridge for Erdős #132 in ordered planar point sets: for all large finite sets, after the unique diameter shell is identified, at least one other sparse distance shell must exist. Anyone assembling the RS route to Erdős #132 cites this Prop as the flux half of the argument. It is a pure proposition definition, not a proved theorem.
Claim. The second-sparse-shell flux bridge is the statement that, for all sufficiently large $n$, every finite planar point set $A$ with $|A|=n$ and every diameter shell distance $\Delta$ of $A$ admits some distance $r\neq\Delta$ that is a sparse shell of $A$.
background
The module physicalizes Erdős problem #132: classical distance values become two-body recognition-energy shells, and shell multiplicity is occupancy. Ordered pairs are used for Lean bookkeeping; for a positive distance the ordered multiplicity is twice the unordered one, so the classical bound $\le n$ becomes $\le 2n$.
A sparse shell is a distance whose ordered multiplicity stays at most linear in $|A|$. A diameter shell is the (unique, nonnegative) shell realizing the maximum pairwise distance. The Hopf–Pannwitz theorem classically supplies that the diameter is already sparse; the RS derivation still needs a second sparse shell once that diameter shell is peeled off.
This declaration packages exactly that residual claim as a named proposition, to be discharged later by shell-flux component or minimal-geometry packages.
proof idea
There is no proof body: the declaration is a bare Prop abbreviation. Its right-hand side is the filter statement “eventually in $n$ at infinity, every $n$-point set whose diameter shell is $\Delta$ carries some sparse shell $r\neq\Delta$.” Downstream closers instantiate this Prop by filter-upwards arguments from component packs or minimal geometry.
why it matters
In the RS reading of Erdős #132, Hopf–Pannwitz gives the first sparse shell (the diameter). The flux bridge is the missing second half: shell-flux conservation after peeling the diameter forces another sparse shell. The parent theorem erdos132_from_hopf_pannwitz_and_flux conjoins a Hopf–Pannwitz hypothesis with this bridge to obtain the ordered Erdős #132 statement. Two closers, from a shell-flux component pack and from a minimal-geometry pack, are the intended discharge routes. The declaration therefore sits at the interface between classical discrete geometry and the RS shell-occupancy ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.