ApproxContainedInGaussianLikeLattice
plain-language theorem explainer
Predicate: a finite planar point set is approximately carried by a Gaussian-like lattice when all but a fixed error budget of its points lie in the lattice image. Additive-combinatorics and RS inverse-spectrum arguments cite it as the weak containment relation inside the planar norm-fiber rigidity target. Pure definition: an existential large subset with lattice membership via the basis chart. Deliberately weak so density-in-a-box or Freiman variants can replace it later.
Claim. A finite set $A\subset\mathbb{R}^2$ is approximately contained in a Gaussian-like lattice $\Lambda$ with error budget $e\in\mathbb{N}$ if there exists $A_0\subseteq A$ with $|A|\le|A_0|+e$ such that every $a\in A_0$ equals the image of some integer coordinate vector $z\in\mathbb{Z}^2$ under $\Lambda$'s basis map.
background
The module physicalizes Erdős problem #661 as a two-channel range-spectrum question: finite planar channels $P,Q$ couple by Euclidean delay, and the classical distance count is the alphabet size of the cross-coupling spectrum. The RS reading targets rigidity of the square-grid $n/\sqrt{\log n}$ (Landau–Ramanujan) scale in a single positive-definite planar carrier.
Point2 is the Euclidean plane $\mathbb{R}^2$. A Gaussian-like lattice is a rank-two carrier recorded only at inverse-theorem strength: a basis map $(\mathrm{Fin},2\to\mathbb{Z})\to\mathbb{R}^2$, a positive scale, and an integral nonnegative binary quadratic form so that visible squared norm equals scale times that form. Approximate containment is the weak “all but $e$ points lie on the lattice image” relation used by the rigidity target.
proof idea
Definitional, not a proved statement. The predicate expands to existence of a subset $A_0\subseteq A$ whose complement in $A$ has size at most the error budget, with every point of $A_0$ equal to $\Lambda.\mathrm{basis}(z)$ for some $z:\mathrm{Fin},2\to\mathbb{Z}$. No lemmas are applied; downstream goals unfold or apply this Prop directly.
why it matters
Feeds PlanarNormFiberRigidityTarget, the inverse-theorem target left by the RS physicalization: a small cross-norm alphabet at the Landau–Ramanujan scale should force the visible points to be approximately carried by a Gaussian-integer-like lattice. That target is the exact classical lemma needed to turn the RS physical statement into a conventional proof; it is recorded, not asserted proved.
In framework terms this sits in the mathematics layer that rigidifies two-sector planar spectra when true orthogonality is unavailable (single positive-definite carrier). The doc-comment flags the relation as deliberately weak: density-in-a-box, Freiman-isomorphism, or Hausdorff-distance strengthenings can replace it without changing the physical claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.