A uniform Hahn-Banach extension loop: states and decoding

Provenance and hypotheses

This note expands draft §8, especially Lemmas 8.4 and 8.9 and Theorems 8.10-8.11. The strategy also occurs in Theorem 21 of the joint paper, v1. Its purpose here is to display the actual state realizers and decoder, not to claim an unpublished loop theorem. The original sections through Theorem 3 treat the norm-one restriction with its inherited representation. The additional sections below extend the decoder to a general bound and the loop architecture to the literal exact-norm problem without asserting an IVT implementation for its unrestricted local oracle.

Fix a computable real Banach space $X$, a fundamental sequence $(b_n)$ with dense linear span, a closed subspace $A$ given by a dense sequence $(a_i)$, and an evaluation realizer for $f:A\to\mathbb R$ with the promise $\|f\|=1$. Every computation below is uniform in the input presentation. No independence of the $b_n$, no removal of repetitions and no decision about subspace membership is required.

Stage spaces and coherent functionals

Set

$$Y_0=A,\qquad Y_{n+1}=\overline{Y_n+\mathbb Rb_n}.$$

Starting with $f_0=f$, choose $\alpha_n\in I(f_n,Y_n,b_n)$ and extend by the formula

$$f_{n+1}(y+tb_n)=f_n(y)+t\alpha_n,$$

followed, where needed, by the unique continuous extension to the closure. N0002, Propositions 1 and 5 justify this step, including the case $b_n\in Y_n$.

Every stage extends $f$, so the bound $\|f_n\|\leq1$ actually gives $\|f_n\|=1$. Compatibility $f_n|_{Y_m}=f_m$ for $m<n$ follows by induction.

Proposition 1. Uniform reconstruction of a finite stage

From $n$, the original instance and the finite list of admissible real values $\alpha_0,\ldots,\alpha_{n-1}$, one can compute a dense sequence for $Y_n$ and an evaluation realizer for $f_n$ with norm bound 1.

Proof. Enumerate all finite rational combinations with retained generating codes

$$d_{n,m}=\sum_{j=0}^{r}\lambda_j a_{i_j}+\sum_{k<n}\mu_k b_k.$$

These points are dense in $Y_n$. Their values are uniformly computable by

$$f_n(d_{n,m})=\sum_{j=0}^{r}\lambda_j f(a_{i_j})+\sum_{k<n}\mu_k\alpha_k. \tag{1}$$

No unique representation is needed: admissibility guarantees that any two codes for one vector give the same functional value.

To evaluate at $y\in Y_n$ with requested error $2^{-k}$, interleave strict tests until finding $m$ with $\|y-d_{n,m}\|<2^{-(k+1)}$. Approximate (1) to error less than $2^{-(k+1)}$. The norm bound gives total error less than $2^{-k}$. The strict tests are semidecidable because the norm is computable, and density guarantees that one eventually succeeds. Currying this procedure gives the required function-space name.

The one-step state machine

A state is the named tuple

$$(X,A,f,n,\alpha_0,\ldots,\alpha_{n-1}).$$

Its domain consists of tuples for which the recorded values are admissible and coherent. Validity is a promise, not a decidable predicate. A transition computes $(Y_n,f_n)$ using Proposition 1, calls $\operatorname{ExtStep}$ at $b_n$, and appends the returned $\alpha_n$ while incrementing $n$.

There is one oracle call per transition. All other work is computable from the state, so

$$\operatorname{StepHB}\leq_{\mathrm W}\operatorname{ExtStep}\leq_{\mathrm W}\operatorname{CC}_1\leq_{\mathrm W}\operatorname{WKL}.$$

Every legal answer leads to another legal state, by the one-step extension theorem. This “every answer” invariant, rather than merely the existence of one successful chain, is what makes the input valid for the infinite-loop operation.

Proposition 2. A whole run computes an extension

From the original instance and any infinite valid run, compute a total $g:X\to\mathbb R$ with $g|_A=f$ and $\|g\|=1$.

Existence. On $Y_\infty=\bigcup_nY_n$, let $g_\infty(y)=f_n(y)$ for any stage containing $y$. Coherence gives well-definedness. By placing any finite set of vectors in one sufficiently large stage, linearity and the norm bound follow. The union contains every $b_n$ and is dense, so $g_\infty$ extends uniquely by continuity to $X$. Its norm is at most 1 and at least the norm of its restriction $f$, hence exactly 1.

A realizer without stage-membership tests. Given $x\in X$ and requested error $2^{-k}$, enumerate all finite rational combinations of the fundamental sequence and find one

$$q=\sum_{i<N}\beta_i b_i,\qquad \|x-q\|<2^{-(k+1)}.$$

This uses only a dovetailed strict distance search. The run supplies names of the finite set of values $\alpha_i$ involved. Compute

$$g(q)=\sum_{i<N}\beta_i\alpha_i$$

to error less than $2^{-(k+1)}$. Since $\|g\|=1$, the approximation error at $x$ is less than $2^{-k}$. The procedure never asks whether $x$ belongs to any particular $Y_n$, and never assumes that the union is all of $X$ rather than merely dense.

Compiling the state machine into the loop operator

An initial mathematical state is not literally an input to every possible coding of the inverse-limit operator. For the convention

$$h^\infty(q_0)=\{\langle q_0,q_1,\ldots\rangle:q_{i+1}\in U\circ\langle\operatorname{id}\times h\rangle(q_i)\},$$

the input also contains a controller for the universal machine $U$.

Here is a concrete name-level implementation. Let $h$ take an encoded pair $(c,s)$, preserve the integer program-code register $c$, call $\operatorname{StepHB}$ on the state named by $s$, and return $(c,t)$ with $t$ a name of any next state. This wrapper is Weihrauch reducible to $\operatorname{StepHB}$. Choose a fixed controller code $c_*$ for the computable operation

$$(c,t)\longmapsto\langle c,(c,t)\rangle.$$

Use the initial loop input $q_0=\langle c_*,(c_*,s_0)\rangle$. After each oracle answer $(c_*,s_{i+1})$, the universal controller returns $q_{i+1}=\langle c_*,(c_*,s_{i+1})\rangle$. Thus the run contains the whole mathematical state sequence, and its elements can be computably decoded.

This is understood with fixed computable pairing and decoding of names and integer registers; re-encoding a returned register does not require preserving its literal input name. The controller reads its code from the preserved register rather than appealing to an unspecified self-referential program. Proposition 2 then supplies the final postprocessor.

Theorem 3. The norm-one upper bound

For the explicit norm-one problem,

$$\operatorname{HB}^{=1}_X\leq_{\mathrm W}\operatorname{WKL}.$$

Indeed the compiled problem $h$ is reducible to WKL. Monotonicity of the loop operator yields $h^\infty\leq_{\mathrm W}\operatorname{WKL}^\infty$, and the external loop-closure theorem gives $\operatorname{WKL}^\infty\equiv_{\mathrm W}\operatorname{WKL}$. Combine the compilation and decoder above.

The external results used here are Proposition 13 and Corollary 27 of Vasco Brattka, Loops, Inverse Limits and Non-Determinism. The computability of the stage data does not, by itself, prove that infinitely many dependent oracle calls collapse to one; the closure theorem is essential.

Lemma 4. A usable bound without an exact norm

From an evaluation realizer for a bounded linear $f:A\to\mathbb R$, on ambient Cauchy names restricted to $A$, one can uniformly compute a positive rational $M$ with $\|f\|\leq M$. This does not compute $\|f\|$.

Here is the local-realizer argument for the usual equivalent Cauchy representation in which the $j$th rational-vector approximant has distance at most $2^{-j}$ from the named point. Use the canonical name of 0 consisting of zero approximants. Run the evaluator until it produces a rational $q$ approximating $f(0)=0$ to error at most $1/4$. Only finitely many entries of the input point-name have been inspected. Choose $N$ large enough to include all those positions.

Every $y\in A$ with $\|y\|<2^{-(N+1)}$ has a valid name with the same inspected zero prefix: complete the remaining positions by sufficiently accurate rational approximants. The machine produces the same $q$ on this name. Consequently $|f(y)|\leq|q|+1/4\leq1/2$. Scaling any unit vector in $A$ by $2^{-(N+2)}$ gives $\|f\|\leq2^{N+1}$. For example choose $M=2^{N+2}$.

This computation uses the named realizer itself, not an abstract continuity assertion without a modulus. Equivalent standard Cauchy encodings can first be converted to the displayed convention. The algorithm only relies on names of points inside the promised domain and does not decide membership in $A$.

Proposition 5. The same decoder with a general bound

Suppose a coherent run has $f_0=f$ and $\|f_n\|\leq M$ for a known positive rational $M$. The stage and union proofs above remain valid with bound $M$. In each strict-distance search replace $2^{-(k+1)}$ by $2^{-(k+1)}/M$; approximate the resulting dense value with error less than $2^{-(k+1)}$. The evaluation error is then less than $2^{-k}$. Nothing else in the state representation, finite sums or controller needs to change, except retaining $M$ as a register.

If the run additionally satisfies $\|f_n\|=\|f\|$ for every $n$, the decoded extension has norm exactly $\|f\|$. Mathematically the union functional has norm at most $r=\|f\|$, and continuity preserves this bound; restriction to $A$ supplies the reverse inequality. Computationally the decoder only needs $M$, not a Cauchy name of $r$. This separates the information needed for an error estimate from the invariant that proves equality of norms.

Theorem 6. Iterating the literal exact one-step problem

For the evaluator-only exact-norm tasks,

$$\operatorname{HBT}_X\leq_{\mathrm W}\bigl(\operatorname{HBT}^{1}_X\bigr)^\infty.$$

Proof. Compute $M$ using Lemma 4 and start at $Y_0=A$, $f_0=f$. At stage $n$, query the exact-norm oracle $\operatorname{HBT}^{1}_X$ on $(f_n,Y_n,b_n)$. It returns a named functional $f_{n+1}$ on $Y_n+\mathbb Rb_n$ extending $f_n$ with its exact norm. These domains are closed because the old domain is closed and only a finite-dimensional space is added; one may retain the earlier closure notation.

Since $0<\|f_0\|<\infty$ and every stage preserves that norm, every next oracle instance satisfies its domain promise, regardless of which legal extension was returned. Keep either the returned functional name or its value $\alpha_n=f_{n+1}(b_n)$ together with the existing reconstruction data. Proposition 5 computes all subsequent realizers and the final output using the original bound $M$. The controller construction above applies with this new transition oracle. Loop monotonicity then yields the displayed reduction.

No exact norm is supplied or calculated in this proof. The essential invariant is

$$\|f_{n+1}\|=\|f_n\|=\|f\|,$$

which follows from the specification of the exact local oracle, not from a weaker unit bound. Replacing that oracle by the bound-one helper $\operatorname{ExtStep}$ is justified on the norm-one restriction, but not on all evaluator-only inputs.

Thus the loop architecture survives the norm-information issue. What does not follow is the substitution $\operatorname{HBT}^{1}_X\leq_{\mathrm W}\operatorname{CC}_1$ and the resulting unrestricted WKL upper bound. N0007 gives a separate upper bound by recovering the exact norm once and then using the original norm-one loop.

Theorem 6 and Lemma 4 are follow-up expansions supplied in this revision, not passages transcribed from the original draft.

What the proof does not assume

The sequence $(b_n)$ need only have dense linear span. Redundant generators cause no problem. An effective basis or a computable decomposition into “old” and “new” components would be unnecessary additional requirements. Likewise, one does not compute $g$ by an unquantified limit of approximations with no convergence modulus: the displayed norm estimate gives the requested error at every query.

The norm-one input promise is essential to the final equality of norms. For a functional known only to have norm at most 1, the same construction proves existence and computability relative to WKL of an extension bounded by 1, and nothing stronger is asserted here.

Changelog

2026-09-10 - Version 0.2: retain the norm-one proof; add a realizer-based bound, the bound-M decoder and iteration of the literal exact-norm local oracle. Version 0.1 supplied the original stage/controller exposition.