Pith. sign in
module module moderate

IndisputableMonolith.Mathematics.BipartiteDistanceSpectrum

show as:
view Lean formalization →

Defines the squared cross-distance alphabet between two finite planar point sets (channels). The spectrum is the finite set of Euclidean squared distances realized by pairs with one point in each channel. Downstream multiplicity and rigidity results cite this alphabet when counting shell occupancy and when comparing planar versus four-space cross spectra. The module is definitional scaffolding plus elementary finiteness and cardinality lemmas over Mathlib.

claimFor finite $A,B\subset\mathbb{R}^2$, the squared cross-distance spectrum is $\{|a-b|^2:a\in A,\,b\in B\}$. The (unsquared) cross-distance spectrum is the corresponding set of Euclidean lengths. Related objects: the cross-difference set, the image of squared norms under channel maps, and the two-channel range experiment comparing planar and four-dimensional realizations.

background

In discrete geometry a distance shell is the level set of a fixed pairwise Euclidean distance. Here the setting is bipartite: only cross pairs between two finite channels $A$ and $B$ are kept, so the alphabet is the set of realized cross distances rather than the full distance set of $A\cup B$.

The module works primarily with squared distances (exact algebraic values over $\mathbb{Q}$ or number fields) and only secondarily with the positive square roots. Points are modeled as Point2 in the plane and Point4 in four-space so that planar spectra can be compared with higher-dimensional embeddings of the same two channels.

Recognition Science reads a classical distance value as a two-body recognition-energy shell; the alphabet defined here is the discrete support of those shells before multiplicity is counted.

proof idea

Definition module with supporting elementary lemmas. Spectra are introduced as finite sets (images of the Cartesian product $A\times B$ under squared Euclidean distance). Cardinality bounds such as the squared-spectrum size being at most $|A|\cdot|B|$ are immediate from the definition of image. Named experiments (TwoChannelRangeExperiment, planar rigidity, fixed cross distance in four-space) package the same constructions for later comparison arguments; no deep analytic or number-theoretic proof lives in this file.

why it matters in Recognition Science

Feeds DistanceShellMultiplicity, which records the RS physicalization of Erdős problem #132: a classical distance shell becomes a two-body recognition-energy shell whose multiplicity is shell occupancy. By isolating the bipartite (cross-channel) alphabet, this module supplies the exact support on which occupancy is later counted and on which planar-versus-four-space rigidity statements are stated. It sits on the mathematics side of the bridge from combinatorial distance geometry to recognition-energy bookkeeping, without yet invoking the J-cost, $\varphi$-ladder, or forcing chain.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

declarations in this module (16)