# Lipschitz equivalent Banach spaces need not be linearly isomorphic

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Lipschitz Equivalent Separable Banach Spaces Need Not Be Linearly Isomorphic](../../preprints/Lipschitz-Equivalent-Separable-Banach-Spaces-Need-Not-Be-Linearly-Isomorphic-September-24-2026/paper.pdf)
- [Bi-Lipschitz Absorption of $c_0$ Without a Linear Copy of $c_0$](../../preprints/Bi-Lipschitz-Absorption-of-c0-Without-a-Linear-Copy-of-c0-September-26-2026/paper.pdf)

## Scope

The formalized counterexample gives separable real Banach spaces $X,Y$ that are bi-Lipschitz equivalent but not linearly isomorphic. The bijection has lower Lipschitz bound $4/21$ and upper bound $76/25$. The linear obstruction is explicit: $X$ contains a linear isometric copy of $c_0(\ell_2)$, whereas $Y$ contains no bounded linear copy of that space.

The formalized result constructs one separable real Banach space $X$ that is bi-Lipschitz equivalent to $X\times c_0$ but contains no closed linear subspace isomorphic to $c_0$. The same space contains a bi-Lipschitz copy of $c_0$, is bi-Lipschitz universal for separable metric spaces, and is not linearly isomorphic to $X\times c_0$. Thus nonlinear absorption of $c_0$ does not force a linear copy of it.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Bi-Lipschitz equivalent nonisomorphic Banach spaces | [LipschitzEquivalence.lean](../ComparatorChallenges/LipschitzEquivalence.lean) |
| Bi-Lipschitz absorption of $c_0$ | [C0Absorption.lean](../ComparatorChallenges/C0Absorption.lean) |