Nonisomorphic separable Banach spaces at Lipschitz distance one
Ryotaro Tanaka
math.FA
Nov 4, 2026 · v2
TL;DR
The main theorem, existence of nonisomorphic separable Banach spaces at Lipschitz distance one, is formalized in Lean 4 with Mathlib, partly adapting OpenAI's Lean code.
Abstract
We construct nonisomorphic separable real Banach spaces whose multiplicative Lipschitz distance is one. Building on OpenAI's graph-space construction, we arrange two sequences of graph spaces into countably many blocks and form two spaces that differ by a single additional block. This block distinguishes their linear structures: one space contains a complemented copy of $\ell_1(c_0(\ell_2))$, whereas the other does not. By mapping the additional block to increasingly late positions and rearranging the remaining blocks, we obtain homeomorphisms whose Lipschitz constants and those of their inverses tend to one, while both spaces and their norms remain unchanged.
Problem
Do there exist separable real Banach spaces that are not linearly isomorphic but have multiplicative Lipschitz distance exactly one? Earlier constructions gave such spaces only for each prescribed error, with the pair depending on that error.
Approach
Two sequences of weighted graph spaces, following OpenAI's construction, are arranged into countably many blocks via l1- and c0-sums. The two resulting spaces differ by a single additional block. A complemented-subspace obstruction separates them linearly. Moving the extra block to increasingly late positions gives homeomorphisms whose Lipschitz constants tend to one. The main theorem is formalized in Lean 4 using Mathlib.
Results
One space contains a complemented copy of l1(c0(l2)) and the other does not, yet their Lipschitz distance equals one. Theorem 1.1 is machine-checked in Lean 4.35.0 with Mathlib.
