The Concrete Complexity

The Hahn-Banach theorem — extending bounded linear functionals from subspaces to full spaces — is computationally equivalent to Weak König’s Lemma, one of the key principles in reverse mathematics. This was known, but the proof required varying the underlying Banach space. The complexity seemed to come from the generality: different spaces, different extensions, the full sweep of functional analysis.

Brattka and Sorg (arXiv:2603.16802) show that the full computational complexity already lives inside a single, fixed, concrete space: ℓ¹, the space of absolutely summable sequences. You do not need to vary the space. One space contains everything.

Furthermore, the one-step Hahn-Banach extension problem for ℓ¹ is Weihrauch-equivalent to the intermediate value theorem — a result about real-valued functions on an interval. And the two-dimensional restriction is equivalent to the lesser limited principle of omniscience, a basic constructive principle about deciding between two alternatives.

The structural surprise is that abstraction is not the source of difficulty. The Hahn-Banach theorem is not hard because it applies to all Banach spaces. It is hard because even its first concrete instance — extending a functional on a subspace of ℓ¹ — already requires the full computational machinery. The generality of the theorem is a consequence of the difficulty, not its cause.

This inverts the usual intuition about abstract mathematics. We expect concrete instances to be easier than general theorems, with difficulty increasing as scope expands. Here, the concrete case is already maximally difficult. The abstract theorem merely restates what was always present in the single example. Generality added nothing to the computational content — it was all there from the beginning.