PlanarNormFiberRigidityTarget
plain-language theorem explainer
Defines the inverse-theorem target for the planar bipartite distance problem: for all large equal cardinalities n, if two planar n-point sets have cross squared-norm alphabet at most n/sqrt(log n), then both are approximately carried by one Gaussian-integer-like lattice (error n/100). Analysts working Erdős #661 or RS two-channel rigidity would cite it. The body is a pure Prop abbreviation, not a proof.
Claim. For all sufficiently large $n$, every pair of finite planar sets $P,Q\subset\mathbb{R}^2$ with $|P|=|Q|=n$ whose alphabet of squared Euclidean norms of cross-differences has cardinality at most $n/\sqrt{\log n}$ admits a single rank-two Gaussian-like lattice $\Lambda$ that carries all but at most $n/100$ points of each of $P$ and $Q$.
background
The module physicalizes Erdős problem #661 as a two-channel range-spectrum question: finite planar sets $P$ and $Q$ couple by Euclidean delay, and the classical distinct-distance count becomes the size of the cross-coupling alphabet. The positive #661 direction asks whether that alphabet can be $o(n/\sqrt{\log n})$. RS reading suggests the opposite rigidity: in one positive-definite planar carrier, true two-sector orthogonality is unavailable, so the square-grid Landau–Ramanujan scale $n/\sqrt{\log n}$ should force lattice structure.
Point2 is the Euclidean plane $\mathbb{R}^2$. The cross squared-norm alphabet is the image of all differences $p-q$ ($p\in P$, $q\in Q$) under squared Euclidean norm. A Gaussian-like lattice is a rank-two carrier given by an integer coordinate chart basis, a positive scale, and an integral nonnegative binary quadratic form reading visible squared norms. Approximate containment means all but an explicit error budget of the points lie in the lattice image; the notion is deliberately weak so density-in-a-box or Freiman variants can replace it later.
proof idea
There is no proof. The declaration is a def equating a name to a Prop: an eventually-for-all quantifier over $n\to\infty$, universal quantification over equal-cardinality planar finsets, the small-alphabet hypothesis comparing cardinality of the cross squared-norm alphabet to $n/\sqrt{\log n}$, and existence of one Gaussian-like lattice approximately containing both sets with error $n/100$. It packages the classical inverse statement the RS physicalization leaves open.
why it matters
This is the exact classical lemma the module says is needed to convert the RS physical claim on bipartite distance spectra into a conventional proof. Module documentation records that RS expects rigidity at the square-grid scale rather than the $o(n/\sqrt{\log n})$ sparsity of positive Erdős #661: small cross-norm alphabet should force both channels onto one Gaussian-integer-like carrier. No downstream theorems yet consume the target; it stands as the named inverse-theorem interface left by the physicalization. Closing it would discharge the bridge from RS two-channel reading back to analytic number theory on planar distance sets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.