erdos132_from_hopf_pannwitz_and_components
plain-language theorem explainer
Hopf–Pannwitz diameter sparsity plus a shell-flux component package yields the ordered form of Erdős #132: every large enough finite planar point set has two distinct sparse distance shells. Cite this when assembling the RS physicalization of #132 or the executable HTML proof graph. The proof is a one-line composition through the second-sparse-shell flux bridge into the existing Hopf–Pannwitz-plus-flux theorem.
Claim. Assume that for all sufficiently large $n$, every planar $n$-point set has a sparse diameter shell (Hopf–Pannwitz, ordered normalization). Assume also a shell-flux component package whose fields include pair-budget pressure on the diameter shell and low-shell structure. Then for all sufficiently large $n$, every planar $n$-point set admits two distinct sparse distance shells.
background
This 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 occupancy. The development works with ordered pairs for Lean bookkeeping: for positive distances, ordered multiplicity is twice the unordered count, so the classical bound $\le n$ becomes $\le 2n$.
A shell is sparse when its ordered multiplicity stays at most $2n$. The ordered #132 target asserts that every large enough finite planar set has two distinct sparse shells. Hopf–Pannwitz is kept as a classical input: it supplies the diameter shell as the first sparse shell for large $n$. The shell-flux component package bundles the remaining classical bridge fields (pair-budget pressure on the diameter, low-shell structure, and siblings) that together close a second sparse shell via flux.
proof idea
One-line term wrapper. Apply the already-proved Hopf–Pannwitz-plus-flux theorem, feeding it the given Hopf–Pannwitz diameter bound and the flux bridge obtained by running the component package through the second-sparse-shell flux bridge constructor. No new geometry is argued here; the work is pure hypothesis plumbing from components to flux to #132.
why it matters
This is the executable assembly node named in the HTML proof plan: Hopf–Pannwitz plus the full component package discharges ordered Erdős #132. Downstream, the sharper reduced-component theorem reuses it by first coercing a reduced pack into a full component pack, then calling this result. In the RS reading, two distinct sparse shells mean two distinct low-occupancy two-body recognition-energy levels on a large planar configuration; that is the physical content of #132 in this module. It does not itself touch the forcing chain T0–T8 or the RCL, but it closes a named classical bridge inside the mathematics layer that the monolith treats as RS-physicalized discrete geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.