Transporting Hahn-Banach instances and extracting separators

Provenance and scope

This note expands draft Lemmas 9.8 and 9.10, Theorem 9.17, and Remarks 9.18–9.19. The fixed-space reduction is already in Proposition 26 of the joint paper, v1. The forcing gadget is due to Gherardi and Marcone, not a new construction of this note.

The constructed oracle inputs have norm exactly 1. Accordingly, the lower construction works both for the norm-one restriction $\operatorname{HB}^{=1}_{\ell^1}$ and for the unrestricted exact-norm problem $\operatorname{HBT}_{\ell^1}$ with its evaluator-only input convention. The WKL equivalence below is stated only for the norm-one restriction. All subspaces are represented by dense sequences unless stated otherwise.

Proposition 1. Transport along a computable isometry

Let $X,Z$ be computable real Banach spaces and $J:X\to Z$ a computable linear isometric embedding with a computable inverse on its range. From a closed linear subspace $A\subseteq X$ given by positive information and a realizer for $f:A\to\mathbb R$ with $0<\|f\|<\infty$, compute an exact-norm extension instance, without requiring a name of its norm,

$$A'=J(A),\qquad f'=f\circ J^{-1}:A'\to\mathbb R.$$

Any exact-norm extension $G:Z\to\mathbb R$ pulls back to the desired exact-norm extension $G\circ J$ on $X$. Norm-one inputs are a special case.

Proof. If $(a_i)$ is dense in $A$, then $(Ja_i)$ is computable from the input and dense in $J(A)$. Closedness follows because $A$ is complete and $J$ is an isometry into the complete metric space $Z$. For a name of a point in $A'$, apply the inverse realizer and then the realizer of $f$. The input promise ensures that these partial procedures are used on their domains. No membership decision is required. Isometry gives $\|f'\|=\|f\|$. For an exact-norm extension $G$,

$$\|G\circ J\|\leq\|G\|=\|f'\|=\|f\|\leq\|G\circ J\|,$$

where the last inequality follows by restriction to $A$. Thus the pullback preserves the norm. These equalities are a mathematical proof of validity; computing the instance requires only the two realizers and a dense sequence, not computing their common norm.

For a general continuous map, an image dense sequence represents the closure of the image, not necessarily a closed image. Completeness and the isometry are the reason that the image itself is an admissible closed subspace here.

The hypothesis on inverse computation is supplied explicitly for $J_{p,q}$ by N0005, Proposition 3, uniformly in the parameters.

The norm-one gadget instance

Use the space $X_{p,q}$, weights $w_n=2^{-n-1}$ and parameters $\delta_n$ from N0005. Let

$$A_{p,q}=\{x\in X_{p,q}:x_n=(\alpha_n,0)\text{ for every }n\},$$

$$f_{p,q}(x)=\sum_nw_n\alpha_n\quad(x\in A_{p,q}).$$

Finite rational vectors in the first coordinate of each block are dense in this closed subspace. Closedness follows also from continuity of each block-coordinate projection and the equations $\beta_n=0$.

The block norm satisfies $\|(\alpha,0)\|_{\delta_n}=|\alpha|$. Thus the series defining $f_{p,q}$ is absolutely convergent on $A_{p,q}$ and $|f_{p,q}(x)|\leq\|x\|_{p,q}$. The vector supported in block zero with value $(2,0)$ has norm and functional value 1. Hence $\|f_{p,q}\|=1$.

Its realizer can be obtained without a computable coordinate-tail modulus for an arbitrary presented vector: evaluate on the enumerated dense finite rational vectors and use the norm-one strict-distance search of N0004, Proposition 1. All ingredients are computable relative to $(p,q)$.

Proposition 2. The forcing calculation

Let $g:X_{p,q}\to\mathbb R$ be a norm-one extension of $f_{p,q}$, and let $z_n$ have value $(0,1)$ in block $n$ and zero elsewhere. Then

$$n\in\operatorname{range}(p)\Longrightarrow g(z_n)=-w_n,\qquad n\in\operatorname{range}(q)\Longrightarrow g(z_n)=w_n.$$

Proof. The coordinate vector has block norm 1, hence $|g(z_n)|\leq w_n$.

If $\delta_n>0$, let $a_n\in A_{p,q}$ have block $(1+\delta_n,0)$. Then $g(a_n)=w_n(1+\delta_n)$, while the block $(1+\delta_n,\delta_n)$ has norm 1: the two expressions inside the defining maximum both equal 1. Therefore

$$|w_n(1+\delta_n)+\delta_ng(z_n)|\leq w_n.$$

Its one-sided upper inequality yields $\delta_n(w_n+g(z_n))\leq0$. Since $\delta_n>0$, this gives $g(z_n)\leq-w_n$, and the existing absolute bound forces equality.

If $\delta_n<0$, use the block $(1-\delta_n,0)$ instead. The block $(1-\delta_n,\delta_n)$ again has norm 1, giving

$$|w_n(1-\delta_n)+\delta_ng(z_n)|\leq w_n.$$

The upper inequality yields $\delta_n(g(z_n)-w_n)\leq0$, so $g(z_n)\geq w_n$. The absolute bound again forces equality. No sign is imposed when $\delta_n=0$.

This is the calculation from Gherardi–Marcone’s Theorem 8.12, written out to make the dependence on the norm-one promise explicit.

Theorem 3. The reduction and a finite-precision readout

Compute the isometry $J_{p,q}$ from N0005 and the transported instance

$$A'=J_{p,q}(A_{p,q}),\qquad f'=f_{p,q}\circ J_{p,q}^{-1}.$$

Proposition 1 supplies its positive subspace name and functional realizer. Call $\operatorname{HB}^{=1}_{\ell^1}$ once and obtain $G$. The pullback $g=G\circ J_{p,q}$ satisfies Proposition 2. By N0005, fixed readout,

$$G(e_{2n})=-1\quad\text{if }n\in\operatorname{range}(p),\qquad G(e_{2n})=1\quad\text{if }n\in\operatorname{range}(q).$$

For each $n$, compute a rational $r_n$ with $|r_n-G(e_{2n})|<1/4$ and put

$$B(n)=\begin{cases}1,&r_n<0,\\0,&r_n\geq0.\end{cases}$$

The test compares a rational approximation, not an arbitrary real with zero. In the forced negative case the approximation is negative; in the forced positive case it is positive. In the remaining case either bit is permitted. Hence $B$ separates the disjoint ranges.

In particular,

$$\operatorname{SEP}\leq_{\mathrm W}\operatorname{HB}^{=1}_{\ell^1}.$$

The displayed postprocessor uses only $G$, since its readout points $e_{2n}$ are fixed. With the scalar function-space output representation used here, the same argument in fact establishes the strong lower reduction. This is an explicitly derived observation of this exposition, not a claim about the wording of the original draft.

Alternatively, the draft’s scale-dependent decoder approximates $G(Jz_n)$ with error less than $2^{-n-3}$ and compares the resulting rational with $2^{-n-2}$. That also works: the two forced values are $\pm2^{-n-1}$, with a strict gap from the threshold after accounting for the error.

Corollary 4. The norm-one classification

The established equivalence $\operatorname{SEP}\equiv_{\mathrm W}\operatorname{WKL}$, Theorem 3 and N0004, Theorem 3 give

$$\operatorname{HB}^{=1}_{\ell^1}\equiv_{\mathrm W}\operatorname{WKL}.$$

The located-subspace strengthening in the joint paper is not reproduced here as an unpublished result. Our statements retain their explicit norm-one promise and the supplied dense-sequence representation.

Corollary 5. What the lower bound says for unrestricted inputs

Theorem 3 produces only norm-one instances. Passing those same names to $\operatorname{HBT}_{\ell^1}$ therefore gives the same norm-one outputs and the same separator decoder. Consequently,

$$\operatorname{SEP}\leq_{\mathrm{sW}}\operatorname{HBT}_{\ell^1},\qquad \operatorname{WKL}\leq_{\mathrm W}\operatorname{HBT}_{\ell^1}.$$

The first reduction is strong for the same fixed-readout reason as in Theorem 3. No exact norm is added to the oracle’s input representation. A lower reduction is not invalidated because the oracle accepts additional, potentially harder instances.

Corollary 4 must not be relabelled as $\operatorname{HBT}_{\ell^1}\equiv_{\mathrm W}\operatorname{WKL}$ under the unrestricted evaluator-only convention. The upper proof there applies to the norm-one restriction. The separate norm-information discussion in N0007 includes both an obstruction and a proposed upper bound for the unrestricted problem.

References and changelog

Gherardi and Marcone, How incomputable is the separable Hahn-Banach theorem?, Theorems 6.7 and 8.12. Brattka and Sorg, Computability of the Hahn-Banach Theorem Revisited, v1. Expanded source: the working draft, §§9.1–9.3.

2026-09-10 - Version 0.2: generalize transport to arbitrary positive unknown norms and state the lower bound for the literal exact-norm problem; retain the norm-one gadget and classification. Version 0.1 supplied the original expanded reduction.