Erdos661Positive
plain-language theorem explainer
Positive Erdős #661 packages the claim that two sequences of n-point planar sets can have cross-distance alphabet little-o of the square-grid scale n/sqrt(log n). Combinatorial number theorists and RS analysts of two-channel range spectra would cite the formulation. It is a bare Prop definition: an existential asymptotic statement with no attached proof.
Claim. There exist sequences of finite planar point sets $P_n$ and $Q_n$, each of cardinality $n$ for all sufficiently large $n$, such that $\#\{\|p-q\|: p\in P_n,\, q\in Q_n\}=o\bigl(n/\sqrt{\log n}\bigr)$ as $n\to\infty$.
background
The module physicalizes Erdős problem #661 as a two-channel range-spectrum question. Two finite planar channels $P$ and $Q$ couple by Euclidean propagation delay; the classical distinct-distance count is the alphabet size of the cross-coupling spectrum.
crossDistSpectrum is the unsquared distance alphabet: the image of the product $P\times Q$ under Euclidean distance. Squaring is algebraically cleaner, but both alphabets carry the same asymptotic information away from sign issues because distance is nonnegative. Points live in the visible plane (Point2).
The positive direction asks whether that alphabet can be $o(n/\sqrt{\log n})$, the square-grid scale. The RS reading in the module header suggests the opposite target: in a single positive-definite planar carrier, true two-sector orthogonality is unavailable, so the grid scale should be rigid.
proof idea
No proof body: the declaration is a Prop definition. It packages an existential claim over two sequences of finite planar point sets, requiring eventual cardinality $n$ along atTop, together with a Tendsto statement that the normalized cross-distance alphabet cardinality tends to $0$ in a neighborhood of zero. The normalizing denominator is exactly the square-grid scale $n/\sqrt{\log n}$. Downstream work either proves this Prop or refutes it via the sibling rigidity target.
why it matters
In RS terms this is the optimistic combinatorial side of the bipartite distance spectrum. The module explicitly contrasts it with the negative RS target (planar cross-spectrum rigidity at the grid scale), recorded as the sibling PlanarCrossSpectrumRigidity. The physical claim is that a single positive-definite planar carrier cannot support true two-sector orthogonality, so the alphabet should not drop below the grid scale.
No downstream theorems yet consume the Prop (used_by is empty). It stands as the named positive interface against which the rigidity program is measured. It does not itself invoke the forcing chain (T0–T8), RCL, or the mass ladder; it is pure discrete geometry placed in the RS two-channel language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.