Linear c0 detection from bi-Lipschitz absorption
Status OpenLLM status Open unverified
Top Open Problems unknownunknown Not reported cataloguedOpenOpenStatement
Definitions and mathematical statement
Statement recorded in the supplied source.
If a separable real Banach space Z is bi-Lipschitz equivalent to Z direct-sum-infinity c0, must Z contain a closed linear subspace isomorphic to c0?Short English statement
If a separable real Banach space Z is bi-Lipschitz equivalent to Z direct-sum-infinity c0, must Z contain a closed linear subspace isomorphic to c0?Sources
- S1 OpenAI, manuscript citation page. Source of the formulation motivating this local problem. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Bi-Lipschitz-Absorption-of-c0-Without-a-Linear-Copy-of-c0-September-26-2026/README.md.
Statement licence: CC-BY-4.0 · Source file
Contributions 1
OpenAI claim summary for Math-2697
The displayed question has a negative answer under the manuscript's stated construction. Its counterexample meets the conditions in this problem and defeats the universal assertion, so this is a full disproof claim. The supporting result is manuscript 1 (family 324; 2026-09-26).
Linear c0 detection from bi-Lipschitz absorption
OpenAI's claim
OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 324; 2026-09-26), the asserted result is that a separable real Banach space with no linear copy of $c_0$ is bi-Lipschitz equivalent to its $c_0$ sum and contains bi-Lipschitz images of every separable metric space.Mathematical statement of the claimed result
Manuscript 1.
Let $c_0$ be real null sequences with the supremum norm, and use the maximum norm on a direct sum. The manuscript claims existence of a separable real Banach space $Z$ and a surjective map \[ F:Z\oplus_{\infty} c_0\longrightarrow Z \] that is bi-Lipschitz, although no closed linear subspace of $Z$ is linearly isomorphic to $c_0$. Thus this absorption is metric rather than a linear direct-sum identity.Outline of the argument
For manuscript 1 (family 324; 2026-09-26), a state-dependent coordinate shift is made onto by finite-dimensional terminal correction. Molecule norms combine selected Lipschitz tests with exponents tending to one in an outer square sum; compatible detectors rule out a linear $c_0$ basis while retaining nonlinear absorption.Formal verification
For manuscript 1 (family 324; 2026-09-26), OpenAI lists Lean statements for this assertion: a separable real Banach space with no linear copy of $c_0$ is bi-Lipschitz equivalent to its $c_0$ sum and contains bi-Lipschitz images of every separable metric space.The central assertion is within the documented formal scope; the additional applications retain their own scope limits.
The linked family Comparator checks are C0Absorption.lean, LipschitzEquivalence.lean.
Their named declarations include OAI.C0Absorption.main_result, OAI.LipschitzCounterexample.main.
This site has not executed the Lean code. Described statement coverage is not an independent proof check.
Status caveat
The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.Sources
- OpenAI, Bi-Lipschitz Absorption of c${}_{0}$ Without a Linear Copy of c${}_{0}$, 2026-09-26; citation key
OAI:Bi-Lipschitz-Absorption-of-c0-Without-a-Linear-Copy-of-c0-September-26-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main. - Family 324: Lean scope.
- Comparator C0Absorption.json.
- Comparator C0Absorption.lean.
- Comparator LipschitzEquivalence.json.
- Comparator LipschitzEquivalence.lean.
- OpenAI catalogue entry.