Complete bipartite embeddings, lattice non-embeddability, and non-Euclidean powers of information distance
Fengqi Hou
cs.IT
Sep 30, 2026 · v1
TL;DR
Main theorems on scale-embeddings and Hilbert non-representability of information distance are accompanied by a Lean formalization checked by the kernel.
Abstract
We encode the vertices of every finite complete bipartite graph as binary strings at each scale. The information distances between these strings approximate the scaled graph distances with an additive error bounded by a constant independent of the scale. We also assign one fixed infinite binary sequence to each vertex; suitable prefixes satisfy the same distance estimate with logarithmic error. This extends Hutter's construction for $K_{3,3}$ and resolves his open problem on scale-embeddings of finite complete bipartite graphs. Combined with his complete bipartite obstruction, these embeddings show that no positive power of information distance can be represented exactly by distances in a real Hilbert space, resolving his question about such representations. For conditional prefix complexity, we further prove that at most $2^{δ+C}$ strings lie between any two strings with total distance exceeding their mutual distance by at most $δ$, where $C$ is independent of the endpoints. This bound rules out scale-embeddings of the integer line and every positive-dimensional integer lattice, resolving Hutter's lattice embedding problem for both string and sequence embeddings. Restriction to the integer lattice gives the same conclusion for $(\mathbb R^m,\|\cdot\|_1)$ for every $m\ge1$.
Problem
Hutter posed open problems on whether finite complete bipartite graphs and integer lattices admit scale-embeddings into information distance (prefix Kolmogorov complexity). He also asked whether positive powers of information distance can be represented exactly by distances in a real Hilbert space.
Approach
Vertices of K_{m,n} are encoded as concatenated products of direction vectors with 2x2 matrices over a finite field F_{2^r}. This yields string embeddings with constant error and sequence embeddings with logarithmic error. Combining these embeddings with Hutter's balanced bipartite obstruction rules out Hilbert representations. A prefix-complexity interval bound limits how many strings lie between two endpoints, which excludes lattice embeddings. The accompanying Lean formalization was written by ChatGPT and checked by the Lean kernel.
Results
Every finite complete bipartite graph admits string and sequence scale-embeddings, and no positive power of information distance is Euclidean. The integer line, every positive-dimensional integer lattice, and (R^m, l1) admit no scale-embeddings, resolving Hutter's Open Problems 37 and 39 and his lattice embedding problem.
