Exact norms and evaluator-only Hahn-Banach inputs

Status, origin and precise convention

This is an additional follow-up analysis, not an omitted section of the source draft. It records proposed deductions concerning the evaluator-only convention, separates exact norms from usable bounds, and reconnects that convention to the expanded interval and loop proofs. The deductions require author verification and attribution review before release. They are not presented as an independently verified erratum or as a literature-wide novelty claim.

We use the literal input and output convention of Definition 15 of Brattka-Sorg, arXiv:2603.16802v1. Fix a computable real Banach space $X$. A closed subspace $A$ is supplied by a dense sequence; a bounded linear $f:A\to\mathbb R$ is supplied by an evaluation realizer on ambient Cauchy names promised to name points of $A$. Its norm is positive and finite but is not a separate input. Both the full problem $\operatorname{HBT}_X$ and the one-step problem $\operatorname{HBT}^{1}_X$ require exact norm preservation. A realizer may also happen to work off its promised domain. In the one-step problem $x\in A$ is allowed.

The notation $\operatorname{HB}^{=1}_X$ used elsewhere means the inherited norm-one restriction of this same problem. A known-norm variant, by contrast, adds a Cauchy name of the exact norm to the input. Confusing a restriction, an enriched representation and a prescribed-bound output task would change the mathematical claim.

Proposition 1. The norm is uniformly accessible from below

Define the norm-recovery operation

$$\operatorname{Norm}_X(A,f)=\|f\|,$$

with the evaluator-only input representation just described and the usual Cauchy representation on the output real. Then

$$\operatorname{Norm}_X\leq_{\mathrm W}\lim.$$

Proof. Let $(a_i)$ be the named dense sequence in $A$, and set

$$c_i=\frac{|f(a_i)|}{\max\{1,\|a_i\|\}}.$$

All $c_i$ are uniformly computable reals relative to the input. The denominator is at least 1, so no nonzero test is needed. The radial map $a\mapsto a/\max\{1,\|a\|\}$ is continuous and fixes every point of the closed unit ball of $A$. Its image of the dense sequence is therefore dense in that ball. It follows that

$$\|f\|=\sup_i c_i.$$

For a fully explicit increasing rational approximation, compute rationals $q_{i,s}$ with $|q_{i,s}-c_i|<2^{-s}$ for $i\leq s$. Start at $r_{-1}=0$ and put

$$r_s=\max\bigl(\{r_{s-1},0\}\cup\{q_{i,s}-2^{-s}:i\leq s\}\bigr).$$

Then $0\leq r_s\leq\|f\|$, the sequence increases, and its supremum is $\|f\|$. There is no claimed computable convergence modulus. The Monotone Convergence Theorem as a represented operation is equivalent to $\lim$; apply it to $(r_s)$ to obtain a Cauchy name of the norm.

The external equivalence used here is Fact 11.26 in Brattka-Gherardi-Marcone, The Bolzano–Weierstrass Theorem is the Jump of Weak König’s Lemma. The application to this specific norm-recovery operation is supplied in this note.

Proposition 2. Reusing the interval and loop proofs without changing the input

For the literal evaluator-only tasks,

$$\operatorname{HBT}^{1}_X\leq_{\mathrm W}\operatorname{CC}_1\star\lim,$$

$$\operatorname{HBT}_X\leq_{\mathrm W}\operatorname{WKL}\star\lim.$$

Here $P\star Q$ is the compositional product: the right factor $Q$ is used first, and the next instance can depend on its answer. These are upper bounds, not asserted exact classifications.

Proof. First apply Proposition 1 to recover $r=\|f\|>0$. Retain the original input name as well. Since division by a positive named real is computable, $h=f/r$ has a uniformly computable realizer relative to these data and satisfies $\|h\|=1$. No further norm recovery is needed at later stages.

For one step, use N0002, Corollary 4 and Proposition 5 to choose the extension value for $h$ and reconstruct the functional $u$ on $A+\mathbb Rx$. Then $g=ru$ extends $f$ and has norm exactly $r$.

For the full problem, use N0004, Theorem 3 on $h$. Its coherent norm-one loop gives a total extension $u$ with $\|u\|=1$. Rescale to $g=ru$. As a Type-2 computation, this is streaming relative to the Cauchy name returned by the norm oracle; it is not an instruction to wait for an entire infinite name to finish.

Rescaling an evaluator is effective: choose a rational $R>r$; to approximate $ru(x)$ to error $\varepsilon$, first bound $|u(x)|$ by a named upper bound for $\|x\|$, then request sufficiently accurate rational approximations to both factors. Standard computable real multiplication performs the same calculation.

The right factor of the compositional product is indispensable in this proof. The computed increasing sequence $(r_s)$ alone does not provide a valid exact norm at any finite stage. Nor may one apply the loop-closure theorem to erase the norm-recovery step: that theorem concerns iterating WKL, not arbitrary limits followed by WKL.

For context only, the external identifications in the same Brattka–Gherardi–Marcone paper, Fact 11.26 and Corollaries 11.7 and 11.27, yield

$$\operatorname{WKL}\star\lim\equiv_{\mathrm W}\operatorname{WKL}'. $$

The prime denotes the Weihrauch jump. This note does not prove $\operatorname{HBT}_X\equiv_{\mathrm W}\operatorname{WKL}'$, nor that the norm-recovery route is optimal. The construction suffices to give a correct upper bound while retaining the old proof architecture.

Proposition 3. A finite-dimensional obstruction

For the literal evaluator-only, positively represented-domain convention,

$$\operatorname{LPO}\leq_{\mathrm W}\operatorname{HBT}_{\ell^1_2},\qquad \operatorname{LPO}\leq_{\mathrm W}\operatorname{HBT}^{1}_{\ell^1_2}.$$

The same reductions work in $\ell^1$ by using its first two coordinates.

Proof. For a binary sequence $p$, let $E=\operatorname{span}\{e_0\}$, $V=\operatorname{span}\{e_0,e_1\}$, and define

$$A_p=\begin{cases}E,&p=0^{\mathbb N},\\V,&(\exists n)\ p(n)=1.\end{cases}$$

A positive name of $A_p$ is computable from $p$. At each finite stage output the next rational point in a dense enumeration of $E$. Once a 1 is seen, also interleave a dense rational enumeration of $V$. Before such an event all emitted points still belong to the eventual domain; after it the enumeration is dense in $V$. There is no test for the absence of an event.

Use the fixed computable evaluator

$$F(z)=\tfrac12z_0+z_1$$

to name $f_p=F|_{A_p}$. This is a valid function-space name for both possible domains; working on additional inputs outside a promised domain is allowed. The norms are

$$\|f_p\|=\begin{cases}\tfrac12,&p=0^{\mathbb N},\\1,&(\exists n)\ p(n)=1.\end{cases}$$

Both are positive, and every instance even has the same known upper bound 1. Thus adding a bound of 1 to the input would not remove the obstruction. Given any exact-norm extension $g$, the first case gives $|g(e_1)|\leq1/2$, whereas the second case gives $g(e_1)=f_p(e_1)=1$. Compute a rational $q$ with $|q-g(e_1)|<1/8$. If $p=0^{\mathbb N}$, then $q<5/8$; if a 1 occurs, then $q>7/8$. The rational test $q>3/4$ therefore decides whether $p$ contains a 1, an equivalent convention for LPO.

For the one-step problem always supply $x=e_1$. In either branch the output domain is $V$, so evaluation at $e_1$ is legal. The second branch uses $x\in A_p$, which the specified problem explicitly permits. In infinite-dimensional $\ell^1$, use the same fixed two-dimensional $V$ for the domains; for the full problem the extension is defined on all of $\ell^1$, and the same readout works.

This is a uniform family of computable transformations relative to $p$. It does not claim that one particular fixed finite-dimensional instance has no computable solution.

Corollary 4. Which upper claims cannot be retained

A single-valued operation into a computable metric space reducible to WKL is computable; see Brattka–Gherardi, Weihrauch Degrees, Omniscience Principles and Weak Computability, Corollary 8.8 in the arXiv version. LPO is not computable: a finite observed all-zero prefix cannot determine that no later 1 occurs.

Thus Proposition 3 rules out a WKL upper bound for either literal problem on $\ell^1_2$ or $\ell^1$. In particular, it also rules out a $\operatorname{CC}_1$ upper bound for the unrestricted exact one-step problem, since $\operatorname{CC}_1\leq_{\mathrm W}\operatorname{WKL}$.

This is an obstruction to the claim with these hypotheses, not merely a failure of one proof attempt. It does not invalidate the classical Hahn–Banach theorem, the supplied-bound interval lemma, the norm-one restrictions, or the norm-one lower constructions. The family does not give computable located subspaces uniformly in $p$, so it makes no corresponding claim for the paper’s located-domain variants.

What must not be substituted for norm recovery

An upper bound $M\geq\|f\|$ does not produce a Cauchy name of $\|f\|$. It only supplies a Lipschitz bound. Extending $f/M$ with norm at most 1 and rescaling produces an extension bounded by $M$, which need not be norm-preserving.

The lower approximations $r_s$ from Proposition 1 cannot be used as provisional bounds in exact interval certificates. They need not bound $f$ at all, so a provisional admissible interval can even be empty. Once an interval has been enumerated as excluded from a negatively represented set, it cannot later be retracted.

Starting with a bound-$M$ full extension $g$ and rescaling it afterwards is not a general repair either: multiplying by $c\ne1$ changes the restriction from $f$ to $cf$. The original problem excludes the zero functional.

Adding an extra summand with a functional that attains the upper budget can force norm 1 on an enlarged auxiliary instance, but restricting the resulting extension back only retains that budget. It does not automatically restore the smaller original norm.

Relationship to the retained proofs

The geometric construction in N0003 and the forcing construction in N0006 already prove exact norm 1 for all their inputs. They can be passed to the general exact-norm oracle unchanged. Their lower reductions therefore survive without using Proposition 1.

N0004 also proves directly that $\operatorname{HBT}_X\leq_{\mathrm W}(\operatorname{HBT}^{1}_X)^\infty$, without recovering the norm, provided the local oracle is the exact one-step operation. The additional norm-recovery route in Proposition 2 serves a different purpose: it bounds the unrestricted problem using familiar benchmark operations while reusing the expanded bound-one interval proof and norm-one loop.

None of these modifications replaces the tree/free-space proof by the paper’s other interval construction, and none replaces the detailed state decoder by a different Hahn–Banach proof.

References and changelog

Brattka and Sorg, Computability of the Hahn-Banach Theorem Revisited, arXiv:2603.16802v1, Definitions 13 and 15, used solely to fix the input/output convention.

Brattka, Gherardi and Marcone, The Bolzano-Weierstrass Theorem is the Jump of Weak König’s Lemma, arXiv:1101.0792, Fact 11.26 and Corollaries 11.7 and 11.27, for external limit and jump identifications.

Brattka and Gherardi, Weihrauch Degrees, Omniscience Principles and Weak Computability, arXiv:0905.4679, Corollary 8.8 in the arXiv version, for the single-valued WKL principle.

Brattka, Loops, Inverse Limits and Non-Determinism, arXiv:2501.17734v1, for the external loop machinery used in N0004.

2026-09-10 - Version 0.1: proposed norm-recovery reduction, explicit exact-norm upper bounds, finite-dimensional obstruction and connection to the retained proofs.