# Compact counterexamples to bi-Lipschitz dimension reduction

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

- [A doubling Hilbert subset with no finite-dimensional bi-Lipschitz embedding](../../preprints/A-doubling-Hilbert-subset-with-no-finite-dimensional-bi-Lipschitz-embedding-September-25-2026/main.pdf)

## Scope

The formalized result gives a doubling subset of real $\ell_2$, with doubling constant at most $76800$, that admits no bi-Lipschitz embedding into any finite-dimensional Euclidean space at any finite distortion. A companion gives one universal doubling constant such that every infinite-dimensional real Banach space contains a compact doubling subset with no bi-Lipschitz embedding into any finite-dimensional normed space.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Doubling Hilbert subset without finite-dimensional embedding | [DoublingHilbert.lean](../ComparatorChallenges/DoublingHilbert.lean) |
| Compact counterexamples in infinite-dimensional Banach spaces | [CompactBanach.lean](../ComparatorChallenges/CompactBanach.lean) |