normSqImage
plain-language theorem explainer
Squared-norm alphabet of a finite planar set: the finite collection of values ‖p‖² for p in A. Anyone packaging a two-channel cross-difference set into a real spectrum cites this. Defined as the classical Finset image under the planar squared-norm map.
Claim. For a finite set $A \subset \mathbb{R}^2$, write $\mathrm{normSqImage}(A) := \{\|p\|^2 : p \in A\} \subset \mathbb{R}$.
background
The module physicalizes Erdős problem #661 as a two-channel range-spectrum question: finite planar channels $P$ and $Q$ couple by Euclidean delay, and the classical distance count is the alphabet size of the cross-coupling spectrum. Points live in the visible planar carrier Point2, the Euclidean space $\mathbb{R}^2$.
The sibling map normSq sends $p$ to $|p|^2$. Upstream amplitude and Hilbert-display squared norms are Born-weight analogues in the recognition calculus; here the same name is the ordinary Euclidean squared length on the plane. The present definition lifts that scalar map to finite sets, producing the discrete alphabet of squared lengths realized by $A$.
proof idea
One-line definition: under classical choice, return the Finset image of $A$ under the planar squared-norm map $p \mapsto |p|^2$. No lemmas beyond Finset.image.
why it matters
Feeds crossNormSqAlphabet, which is exactly this image applied to the cross-difference set $Q-P$. That alphabet is the squared form of the bipartite distance spectrum the module studies. In the RS reading of Erdős #661, true two-sector orthogonality is unavailable in a single positive-definite planar carrier, so the square-grid $n/\sqrt{\log n}$ scale is expected to be rigid; packaging cross-differences as a squared-norm alphabet is the first bookkeeping step toward that inverse-theorem target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.