Bounded approximation in uniformly discrete Lipschitz-free spaces

Bounded approximation in uniformly discrete Lipschitz-free spaces

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 330; 2026-09-26), the asserted result is that a countable uniformly discrete metric space has a real Lipschitz-free space with the approximation property but without any bounded approximation constant.

Mathematical statement of the claimed result

Manuscript 1.

For a pointed metric space $(M,d,o)$, let $\mathcal F(M)$ be the closed span of evaluation functionals $\delta_x$ in the dual of real Lipschitz functions vanishing at $o$. The claim supplies a countable unbounded nonproper space with \[ d(x,y)\ge1\ (x\ne y),\qquad \mathcal F(M)\text{ has AP but fails }\lambda\text{-BAP for every finite }\lambda\ge1. \] AP means uniform approximation of the identity on compact sets by finite-rank operators; $\lambda$-BAP additionally bounds their norms by $\lambda$. Thus uniform discreteness does not force bounded approximation for the free space.

Outline of the argument

For manuscript 1 (family 330; 2026-09-26), colored-graph blocks carry signed measures and opposing local bump tests that force large finite-rank norms. Each block still admits coefficient truncation, but a metric wedge joins blocks with unbounded required constants, preserving AP and defeating BAP.

Formal verification

For manuscript 1 (family 330; 2026-09-26), OpenAI lists Lean statements for this assertion: a countable uniformly discrete metric space has a real Lipschitz-free space with the approximation property but without any bounded approximation constant.

The central assertion is within the documented formal scope; the additional applications retain their own scope limits.

The linked family Comparator checks are DiscreteLipschitzFree.lean, RealL1Renorming.lean.

Their named declarations include OAI.DiscreteFree.real_l1_quantitative_renorming, OAI.DiscreteFree.source_endpoints.

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, A uniformly discrete counterexample to bounded approximation in Lipschitz-free spaces, 2026-09-26; citation key OAI:Failure-of-Bounded-Approximation-in-a-Lipschitz-Free-Space-over-a-Uniformly-Discrete-Metric-Space-September-26-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main.
• Family 330: Lean scope.
• Comparator DiscreteLipschitzFree.json.
• Comparator DiscreteLipschitzFree.lean.
• Comparator RealL1Renorming.json.
• Comparator RealL1Renorming.lean.
• OpenAI catalogue entry.