Effective one-step Hahn-Banach intervals

Provenance and exact task

This note expands draft Definitions 7.1 and 7.4, Lemmas 7.2-7.6 and Proposition 7.8, together with the dense-evaluation idea of Lemma 8.4. Propositions 1-5 concern a prescribed bound of 1, not norm preservation for an arbitrary functional of unknown norm. Proposition 6 extends the same certificate proof to any supplied positive bound. The main exact-norm problem retains the paper’s evaluator-only input convention, as specified in N0001. The general one-step result is classical; compare Theorem 6 and Proposition 20 of the joint paper, v1.

Fix a computable real Banach space $X$. The input consists of a closed linear subspace $Y$ with a dense sequence $(y_i)$, a bounded linear $f:Y\to\mathbb R$ given by an evaluation realizer with the promise $\|f\|\leq1$, and $x\in X$. Define

$$I(f,Y,x)=\{\alpha:\exists g:Y+\mathbb Rx\to\mathbb R\text{ linear},\ g|_Y=f,\ g(x)=\alpha,\ \|g\|\leq1\}.$$

Proposition 1. The classical admissible interval

Set

$$L=\sup_{y\in Y}\bigl(f(y)-\|y-x\|\bigr),\qquad U=\inf_{y\in Y}\bigl(\|y+x\|-f(y)\bigr).$$

Then $-\|x\|\leq L\leq U\leq\|x\|$, and $I(f,Y,x)=[L,U]$. For every $\alpha$ in this interval,

$$g(y+tx)=f(y)+t\alpha$$

is a well-defined linear extension with norm at most 1, including when $x\in Y$.

Proof. The bound on $f$ and the reverse triangle inequality give

$$f(y)-\|y-x\|\leq\|x\|,\qquad \|y+x\|-f(y)\geq-\|x\|.$$

Using $y=0$ gives the other finite bounds on $L$ and $U$. For $y,z\in Y$,

$$f(y)+f(z)=f(y+z)\leq\|y+z\|\leq\|y-x\|+\|z+x\|,$$

so $L\leq U$. If $\alpha\in[L,U]$, then

$$f(y)+\alpha\leq\|y+x\|,\qquad f(y)-\alpha\leq\|y-x\|.$$

For $t>0$ apply the first inequality to $y/t$ and multiply by $t$. For $t<0$ write $t=-s$, apply the second inequality to $y/s$ and multiply by $s$. The case $t=0$ follows from the bound on $f$. Applying the resulting one-sided estimate also to $(-y,-t)$ yields

$$|f(y)+t\alpha|\leq\|y+tx\|. \tag{1}$$

If $y+tx=y'+t'x$, apply (1) to $(y-y',t-t')$. The two proposed values of $g$ agree. Linearity and the norm bound now follow directly. Conversely, any admissible extension applied to $y+x$ and $y-x$ gives $\alpha\leq U$ and $\alpha\geq L$. This proves the claim.

Changing $y$ to $-y$ shows that the upper bound can equivalently be written as $\inf_y(f(y)+\|x-y\|)$. This change of notation is not a different extension theorem.

Proposition 2. Inequality characterization

For any real $\alpha$,

$$\alpha\in I(f,Y,x)\quad\Longleftrightarrow\quad(\forall y\in Y)(\forall t\in\mathbb R)\ |f(y)+t\alpha|\leq\|y+tx\|.$$

The forward implication is evaluation of the extension. The reverse implication is exactly the well-definedness and norm argument for (1). This formulation avoids a membership test for $x\in Y$.

Proposition 3. Computing negative information

Uniformly from the input, one can compute a rational $B>0$ with $\|x\|\leq B$ and enumerate rational open intervals whose union, relative to $[-B,B]$, is its complement of $I(f,Y,x)$.

Proof. Obtain a rational $q$ with $|q-\|x\||<1$ and put $B=|q|+1$. Dovetail all tuples

$$(i,t,c,k)\in\mathbb N\times(\mathbb Q\setminus\{0\})\times\mathbb Q\times\mathbb N.$$

For each tuple semidecide

$$|f(y_i)+tc|>\|y_i+tx\|+2^{-k}. \tag{2}$$

Both real quantities are computable relative to the input. In particular, if rational approximations $a_m,b_m$ to $f(y_i),\|y_i+tx\|$ have errors less than $2^{-m}$, accept once

$$|a_m+tc|-2^{-m}>b_m+2^{-m}+2^{-k}.$$

When (2) is certified, emit the rational open interval $(c-\varepsilon,c+\varepsilon)$, where

$$\varepsilon=\frac{2^{-k}}{2(|t|+1)}.$$

The representation interprets this open interval relative to $[-B,B]$; do not encode its clipped intersection as though it necessarily had rational-open endpoints in $\mathbb R$.

For $|\alpha-c|<\varepsilon$,

$$|f(y_i)+t\alpha|>\|y_i+tx\|+2^{-k}-|t|\varepsilon>\|y_i+tx\|.$$

Proposition 2 shows that the emitted interval contains no admissible value.

For coverage, fix $\alpha_*\in[-B,B]\setminus I(f,Y,x)$. Proposition 2 supplies $y,t$ with a positive violation

$$\eta=|f(y)+t\alpha_*|-\|y+tx\|>0.$$

Necessarily $t\ne0$. Choose $k$ with $2^{-k}<\eta/8$, then choose $y_i$ and rational nonzero $t_0$ such that

$$\|y_i-y\|<\eta/16,\qquad |t_0-t|<\eta/(16B).$$

Using $\|f\|\leq1$ and $|\alpha_*|,\|x\|\leq B$, the violation at $(y_i,t_0,\alpha_*)$ exceeds

$$\eta-2\|y_i-y\|-2B|t_0-t|>\eta/2>4\cdot2^{-k}.$$

Choose rational $c$ with $|c-\alpha_*|<2^{-k}/(4(|t_0|+1))$. Moving from $\alpha_*$ to $c$ loses less than $2^{-k}/4$ in the left-hand side, so (2) holds. Moreover $\alpha_*$ lies in the emitted interval. Thus every inadmissible point is covered.

All searches are interleaved; the procedure never waits forever for one failed test before trying another. If no interval is emitted for a while, a standard negative-name encoding allows padding. A negative name need not enumerate any nonempty interval when the complement is empty.

Corollary 4. Reduction to interval choice

The affine map

$$h_B(\alpha)=\frac{\alpha+B}{2B}$$

transforms the negatively represented nonempty interval $I(f,Y,x)$ into one in $[0,1]$. Its inverse is $h_B^{-1}(u)=2Bu-B$. Mapping complement intervals gives a computable preprocessor and the inverse gives a computable postprocessor. Hence

$$\operatorname{ExtStep}_X\leq_{\mathrm W}\operatorname{CC}_1\equiv_{\mathrm W}\operatorname{IVT}.$$

The last equivalence is an external theorem, not proved here; see Brattka–Le Roux–Miller–Pauly.

Proposition 5. From the chosen scalar to a functional realizer

Given an admissible $\alpha$, one can compute positive information for $Z=\overline{Y+\mathbb Rx}$ and a realizer for the unique continuous extension of $g$ to $Z$, with norm bound 1.

Enumerate all finite rational combinations of the $y_i$ and $x$. If a combination has the displayed code

$$d_m=\sum_{j=0}^{r}\lambda_j y_{i_j}+t x,$$

its functional value is computable as $\sum_j\lambda_j f(y_{i_j})+t\alpha$. Different codes for the same point give the same value by Proposition 2; linear independence is unnecessary.

Given a name of $z\in Z$ and a requested error $2^{-k}$, dovetail the strict distance tests until some $m$ satisfies $\|z-d_m\|<2^{-(k+1)}$. Approximate $g(d_m)$ with error less than $2^{-(k+1)}$. The total error is less than $2^{-k}$. This also constructs a function-space name by the usual parameterization of Type-2 realizers.

For closed $Y$, the space $Y+\mathbb Rx$ is already closed: it is the preimage, under the quotient map to $X/Y$, of the finite-dimensional span of the coset of $x$. The closure notation makes the algorithm’s completion step explicit and does not require deciding whether a dimension was actually added.

Proposition 6. A supplied bound and the exact-norm specialization

Suppose a positive real $M$ is supplied by a Cauchy name, with the promise $\|f\|\leq M$. Define

$$I_M(f,Y,x)=\{\alpha:\exists g:Y+\mathbb Rx\to\mathbb R\text{ linear},\ g|_Y=f,\ g(x)=\alpha,\ \|g\|\leq M\}.$$

Then

$$I_M(f,Y,x)=M I(f/M,Y,x)=[L_M,U_M],$$

where

$$L_M=\sup_{y\in Y}\bigl(f(y)-M\|y-x\|\bigr),\qquad U_M=\inf_{y\in Y}\bigl(M\|y+x\|-f(y)\bigr).$$

The same proof gives

$$\alpha\in I_M(f,Y,x)\ \Longleftrightarrow\ (\forall y\in Y)(\forall t\in\mathbb R)\ |f(y)+t\alpha|\leq M\|y+tx\|.$$

Computable negative information, with the original certificate method. Choose a rational $B>0$ with $M\|x\|\leq B$. Dovetail strict tests

$$|f(y_i)+tc|>M\|y_i+tx\|+2^{-k}.$$

On success emit $(c-\varepsilon,c+\varepsilon)$, where $\varepsilon=2^{-k}/(2(|t|+1))$, relative to $[-B,B]$. Soundness is unchanged because varying $\alpha$ changes the left-hand side by at most $|t|\,|\alpha-c|$.

For completeness, let $\alpha_*\notin I_M(f,Y,x)$ have a witnessed violation of size $\eta>0$. Moving from $(y,t)$ to $(y_i,t_0)$ loses at most

$$2M\|y_i-y\|+\bigl(|\alpha_*|+M\|x\|\bigr)|t_0-t|\leq2M\|y_i-y\|+2B|t_0-t|.$$

Choose these approximations so that the loss is less than $\eta/2$. The rational-center and margin argument of Proposition 3 then applies without change. Products with the named real $M$ are computable, so the strict tests are semidecidable. The affine normalization from Corollary 4 again gives one call to $\operatorname{CC}_1$.

Functional output. For a requested evaluation error $2^{-k}$, choose a positive rational $\rho$ with $M\rho<2^{-(k+1)}$, search for $\|z-d_m\|<\rho$, and approximate the dense value to error less than $2^{-(k+1)}$. This is the bound-$M$ version of Proposition 5.

Exact norm. Classically, the exact-norm admissible interval is $I_{\|f\|}(f,Y,x)$. If a name of $r=\|f\|>0$ is supplied, take $M=r$. The extension then has norm at most $r$ and at least the norm of its restriction, hence exactly $r$. This proves the known-norm one-step upper bound and, by taking the constant $r=1$, the upper bound for the inherited norm-one restriction $\operatorname{HBT}^{1,=1}_X$.

For the unrestricted evaluator-only input, merely writing $M=\|f\|$ in the formula is not a computable preprocessing step. The lower rational approximations to $\|f\|$ described in N0007 cannot be substituted into the strict certificate test: a provisional violation may disappear when the approximated norm increases, whereas a negative name cannot retract an emitted interval. The known-norm specialization therefore does not assert $\operatorname{HBT}^{1}_X\leq_{\mathrm W}\operatorname{CC}_1$ for arbitrary evaluator-only inputs.

Limits of the assertion

For $\|f\|<1$, these propositions guarantee an extension bounded by 1; they do not guarantee that its norm equals $\|f\|$. When $\|f\|=1$, equality follows because an extension cannot have smaller norm than its restriction. The arguments are uniform relative to a supplied computable Banach-space presentation; they do not assume an effective basis of a subspace or a computable decomposition $z=y+tx$.

References and changelog

The joint paper is arXiv:2603.16802v1. For connected choice, see Brattka, Le Roux, Miller and Pauly, Connected Choice and the Brouwer Fixed Point Theorem, arXiv:1206.4809.

2026-09-10 - Version 0.2: preserve Propositions 1-5 and add the supplied-bound certificate argument and exact-norm specialization. Version 0.1 supplied the original expanded proof.