Pith. sign in
module module moderate

IndisputableMonolith.Mathematics.BipartiteDistanceSpectrum

show as:
view Lean formalization →

Defines the squared and unsquared cross-distance alphabets between two finite planar point channels, together with basic cardinality and rigidity facts. A number theorist or discrete geometer studying bipartite distance sets would cite it; RS uses it as the combinatorial substrate for shell multiplicity. The module is mostly definitional, with short combinatorial lemmas on spectra and fixed distances.

claimFor finite planar channels $A,B\subset\mathbb{R}^2$, the squared cross-distance alphabet is $\{|a-b|^2:a\in A,\,b\in B\}$, and the cross-distance spectrum is the corresponding set of Euclidean lengths. The module also records the four-space fixed-cross-distance problem and related bipartite range experiments.

background

In discrete geometry, a bipartite (cross) distance set is the set of Euclidean lengths realized between two finite point sets rather than within one set. Here the two sets are called planar channels: finite subsets of the plane. The squared alphabet is preferred algebraically because $|a-b|^2$ is a polynomial in the coordinates, while the unsquared spectrum is the geometric object of interest.

The module introduces coordinate types for points in $\mathbb{R}^2$ and $\mathbb{R}^4$, the squared-norm map, the image of that map on cross pairs, and the cross-difference set. These feed cardinality bounds (the spectrum cannot exceed the number of ordered pairs) and rigidity statements about when a prescribed cross-distance configuration can sit in the plane or in four-space.

Downstream, Recognition Science reads each distinct distance value as a two-body recognition-energy shell; the combinatorial alphabet is therefore the discrete support of shell occupancy.

proof idea

Primarily a definition module. Core objects (point types, squared cross-distance spectrum, cross-distance spectrum, norm-squared image, cross-difference set) are introduced by direct set comprehensions. Short lemmas bound the cardinality of the squared spectrum by the number of ordered pairs and record positivity or rigidity facts (Erdős-type positivity, planar cross-spectrum rigidity, fixed cross-distance in four-space) by elementary counting and coordinate algebra rather than deep analytic machinery.

why it matters in Recognition Science

Feeds the module DistanceShellMultiplicity, which is the RS physicalization of Erdős problem #132: classically a distance value is a shell in the pairwise Euclidean distance set; physically it is a two-body recognition-energy shell whose multiplicity is shell occupancy. Without a clean bipartite alphabet, shell occupancy has no combinatorial carrier. The planar and four-space rigidity lemmas constrain which spectra can arise from channels compatible with the $D=3$ spatial forcing (T8) and with two-channel range experiments used later in the mass and coupling ladder. The module therefore sits at the interface between discrete geometry and the recognition-energy reading of distance shells.

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)