Mathematics Bipartite Distance Spectrum Cross Dist Sq Spectrum Card Le Pairs

The counting bound

Take two finite collections of points in the plane, call them P and Q. Consider every pair consisting of one point from P and one point from Q, and compute the squared Euclidean distance between the two points of each pair. Some of these squared distances may coincide. The set of all distinct squared distances that occur is called the cross squared-distance spectrum. The theorem crossDistSqSpectrum_card_le_pairs states a bound on how many distinct squared distances this spectrum can contain: it is at most the number of pairs, which is the size of P multiplied by the size of Q.

This bound is a trivial consequence of the definition. The spectrum is obtained by taking the set of all pairs and mapping each pair to its squared distance. A map from a set to another set can never produce more distinct outputs than the size of the original set. The proof in the machine-checked library of formal theorems verifies this in a few lines, using the standard fact that the image of a finite set under any function has cardinality no larger than the set itself. The bound is sharp in the sense that it can be attained, for instance when all squared distances are distinct.

The declaration also relates to a classical problem in combinatorial geometry. Erdős problem #661 asks whether there exist two n-point sets in the plane whose cross-distance alphabet, the number of distinct distances between the two sets, is o(n / sqrt(log n)), that is, grows slower than n divided by the square root of the natural logarithm of n. The counting bound here does not settle that question. It only gives the trivial upper bound of n squared, which is far larger than the scale in Erdős's problem.

In Recognition Science, the declaration is part of a broader physicalization of the problem. The framework models the two sets as two planar channels, a source set and a detector set, and interprets the distinct cross-distances as the alphabet of a cross-coupling spectrum. The framework's target, called PlanarCrossSpectrumRigidity, predicts that in a single planar carrier the n / sqrt(log n) scale is rigid, meaning the alphabet cannot be made smaller than a constant times that scale. That target is a hypothesis, not a proved theorem, and the counting bound does not imply it.

What the declaration does establish is a clean, machine-checked fact about finite planar sets. It gives a precise upper bound on the number of distinct squared distances between two sets, and it does so in a way that is fully verified. This is the kind of foundational lemma that a larger theory can build on, even though it is too weak by itself to resolve the Erdős problem or to prove the framework's rigidity target.

/-- Trivial upper bound: the cross spectrum has at most one value per
source-detector pair. -/
theorem crossDistSqSpectrum_card_le_pairs (P Q : Finset Point2) :
    (crossDistSqSpectrum P Q).card ≤ P.card * Q.card := by
  classical
  unfold crossDistSqSpectrum
  calc
    ((P.product Q).image (fun pq => dist pq.1 pq.2 ^ 2)).card ≤
        (P.product Q).card := Finset.card_image_le
    _ = P.card * Q.card := by simp

What this page does not claim

The declaration does not prove the Erdős #661 question in either direction. It does not establish the PlanarCrossSpectrumRigidity target. It does not imply any bound tighter than the trivial product of the two set sizes.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Mathematics/BipartiteDistanceSpectrum.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: