GaussianLikeLattice
plain-language theorem explainer
A data package for a rank-two planar lattice carrier: integer coordinates map to the plane, squared Euclidean norms equal a positive scale times a nonnegative integral binary quadratic form. Cited by the approximate-containment predicate and the planar norm-fiber rigidity target for the RS reading of Erdős #661. Pure structure definition; no proof obligations beyond the field predicates.
Claim. A Gaussian-like lattice consists of a map $b:\mathbb{Z}^2\to\mathbb{R}^2$, a scale $s>0$, and an integral binary quadratic form $q:\mathbb{Z}^2\to\mathbb{Z}$ with $q\ge 0$, such that for every lattice vector $z$ one has $\|b(z)\|^2 = s\, q(z)$.
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 is the alphabet size of the cross-coupling spectrum. The positive direction asks whether that alphabet can be $o(n/\sqrt{\log n})$; the RS reading pushes the opposite rigidity at the square-grid Landau–Ramanujan scale.
Point2 is the Euclidean plane $\mathbb{R}^2$. Squared norm is the standard sum of squares. The structure records only what an inverse theorem needs: a proposed Gaussian-integer coordinate chart (basis), a positive real scale, and an integral nonnegative binary quadratic form whose scaled values reproduce visible squared norms (integral_norm). No full lattice-group axioms are imposed at this layer.
proof idea
Definitional structure with no proof body. Field predicates are the positivity of the scale, nonnegativity of the quadratic form on all integer pairs, and the exact scaling identity linking planar squared norm to that form. Downstream predicates quantify over inhabitants of this type.
why it matters
This is the carrier type for the inverse-theorem side of the module. ApproxContainedInGaussianLikeLattice says a finite set is approximately carried by such a lattice (all but an error budget of points lie in the image of basis). PlanarNormFiberRigidityTarget is the exact classical lemma the RS physicalization leaves open: small cross-norm alphabet at the Landau–Ramanujan scale forces visible points to be approximately carried by a Gaussian-integer-like lattice.
In framework terms it packages the single positive-definite planar carrier that blocks true two-sector orthogonality, so the $n/\sqrt{\log n}$ grid scale should be rigid. It does not itself prove Erdős #661; it names the lattice shape the rigidity target talks about.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.