Interval choice through a fixed tree and a fixed hyperplane of the sequence space

Provenance and what is reconstructed

Draft Proposition 7.9 (pp. 14-16) sketches a reduction through one-point Lipschitz extension and a Lipschitz-free space. Its tree metric and prescribed values are the starting point here. The effective passage to a Banach-space instance was explicitly left unresolved in the draft.

The explicit $\ell^1$ model, closed-hyperplane identification, complete realizer and locatedness calculation below are reconstructed additions to this web version, not a transcription of a completed draft proof. The norm-one one-step classification is proved below, together with a lower reduction to the unrestricted problem. This is not a proof of an unrestricted evaluator-only equivalence, and no claim of priority for a new theorem is made. The paper’s comparison point is Proposition 22 of arXiv:2603.16802v1.

Proposition 1. Total endpoint approximations

From negative information for a nonempty closed interval $K=[a,b]\subseteq[0,1]$, compute rational sequences

$$\ell_n\uparrow a,\qquad u_n\downarrow b,\qquad 0\leq\ell_n\leq a\leq b\leq u_n\leq1.$$

Proof. Semidecide, for each rational $q\in[0,1]$, whether the compact interval $[0,q]$ is covered by the enumerated open complement of $K$. A certificate is a finite subcover, whose coverage is decidable for rational intervals. Do the same for $[q,1]$.

At computational stage $n$, run a finite initial portion of these searches for finitely many steps, enlarging both portions with $n$. Let $\ell_n$ be the maximum of 0 and all left certificates found so far; let $u_n$ be the minimum of 1 and all right certificates found so far. Every rational below $a$ and every rational above $b$ is eventually certified on the relevant side. The bounds and limits follow.

This is a stagewise construction, not an instruction to wait for the $n$th enumerated certificate. One side can have no certificates at all, for example when $a=0$ or $b=1$.

The metric gadget

Let $M=\{0,x,s\}\cup\{p_n,q_n:n\in\mathbb N\}$ be the vertices of the rooted tree with edges of lengths

$$d(0,x)=2,\qquad d(0,s)=1,\qquad d(x,p_n)=d(x,q_n)=\tfrac12.$$

All other distances are sums along the unique path in this tree. On $D=M\setminus\{x\}$ prescribe

$$\varphi(0)=0,\quad\varphi(s)=1,\quad\varphi(p_n)=\ell_n+\tfrac12,\quad\varphi(q_n)=u_n-\tfrac12.$$

Here is the complete pair check. Distinct leaves have distance 1. Values within either leaf family differ by at most 1. For a $p$-leaf and a $q$-leaf, including matching indices,

$$|\varphi(p_n)-\varphi(q_m)|=|1+\ell_n-u_m|\leq1,$$

because $0\leq\ell_n\leq u_m\leq1$. The pair $(0,s)$ has value difference and distance 1. A $p$-leaf has value in $[1/2,3/2]$ and a $q$-leaf in $[-1/2,1/2]$, while its distance to 0 is $5/2$ and to $s$ is $7/2$. These estimates cover all remaining pairs. Thus $\varphi$ is 1-Lipschitz, with Lipschitz norm exactly 1.

The admissible values $\alpha$ at $x$ are exactly

$$\bigcap_n[\ell_n,\ell_n+1]\ \cap\ \bigcap_n[u_n-1,u_n]=[a,b].$$

The constraints from 0 and $s$ add $[-2,2]$ and $[-2,4]$, respectively, and hence do not change this intersection.

Proposition 2. An explicit Banach-space realization

Use the fixed space $X=\ell^1(\mathbb N)$ with unit vectors $e_j$ and define

$$v_0=0,\qquad v_x=2e_0,\qquad v_s=e_1,$$

$$v_{p_n}=2e_0+\tfrac12e_{2n+2},\qquad v_{q_n}=2e_0+\tfrac12e_{2n+3}.$$

Then $\|v_z-v_w\|_1=d(z,w)$ for all vertices. In particular the whole metric gadget is represented by fixed rational vectors, independently of $K$.

This is also a concrete realization of the Lipschitz-free space of this particular tree. To see this without assuming an effective theorem about arbitrary metric spaces, give a finite combination of evaluation vectors its free norm

$$\left\|\sum_z c_z\delta(z)\right\|_{\mathcal F(M)}=\sup_{\psi(0)=0,\ \operatorname{Lip}(\psi)\leq1}\left|\sum_z c_z\psi(z)\right|.$$

For each oriented edge, a 1-Lipschitz function has an increment bounded by that edge’s length. Conversely any such assignment of edge increments defines a 1-Lipschitz function on the vertices, because the path distance bounds the sum of its increments. The coordinates of $\sum_zc_zv_z$ are precisely edge length times the sum of coefficients of descendants of that edge. Choosing each edge increment with the sign of the corresponding coordinate realizes the $\ell^1$ norm. Thus $\delta(z)\mapsto v_z$ is an isometry on finite spans.

Its range spans every unit vector:

$$e_0=v_x/2,\quad e_1=v_s,\quad e_{2n+2}=2(v_{p_n}-v_x),\quad e_{2n+3}=2(v_{q_n}-v_x).$$

After completion this is a surjective isometry $\mathcal F(M)\cong\ell^1$. Its action and inverse on these generators are rational and explicit, so both are computable for the associated Cauchy presentations. This settles the draft’s effective question for this tree; it makes no blanket claim about all computable metric spaces.

For the classical background motivating the draft, see Godefroy and Kalton, Lipschitz-free Banach spaces, Studia Mathematica 159 (2003), 121–141. The special effective calculation above is supplied here rather than attributed to that paper.

Proposition 3. A fixed closed hyperplane

Let

$$Y=\overline{\operatorname{span}}\{e_1,v_{p_n},v_{q_n}:n\in\mathbb N\},\qquad \Lambda(z)=z_0-4\sum_{j\geq2}z_j.$$

Then $Y=\ker\Lambda$, $v_x\notin Y$, and $Y+\mathbb Rv_x=X$. Moreover $Y$ has a fixed computable dense sequence and is computably located, with

$$d_Y(z)=\frac{|\Lambda(z)|}{4}.$$

Proof. Every displayed generator is in the kernel. Conversely, for $z\in\ker\Lambda$, truncate the tail coordinates and set the zeroth coordinate of the truncation to four times their sum, keeping $z_1$. The resulting finite vectors are in the algebraic span of the generators. The approximation error is at most five times the discarded $\ell^1$ tail, hence tends to zero. Rational combinations of the fixed generators give positive information for $Y$.

The functional $\Lambda$ has norm 4, and $\Lambda(v_x)=2$. Thus $z-(\Lambda(z)/2)v_x\in Y$, proving $Y+\mathbb Rv_x=X$. For any $y\in Y$, $|\Lambda(z)|\leq4\|z-y\|_1$. Conversely, $z+(\Lambda(z)/4)e_2$ is in $Y$ and is at distance $|\Lambda(z)|/4$. The distance formula follows. Summation on $\ell^1$ is computable from Cauchy names by finite-support approximation and a norm bound; therefore so is $\Lambda$.

Proposition 4. A uniformly computable norm-one functional

Define on $Y$

$$f(z)=z_1+\sum_{n\geq0}\bigl((2\ell_n+1)z_{2n+2}+(2u_n-1)z_{2n+3}\bigr).$$

This functional is computable uniformly from the name of $K$, has norm exactly 1 on $Y$, and satisfies $f(v_z)=\varphi(z)$ for $z\in D$.

Computability. The coefficient sequence is uniformly computable and bounded in absolute value by 3. The formula therefore defines a computable functional on all of $X$ with bound 3, whose restriction is $f$. To obtain error $2^{-k}$, approximate the input by a finite rational vector to error less than $2^{-k}/6$, then evaluate its finite sum to error less than $2^{-k}/2$. The error from the vector approximation is less than $3\cdot2^{-k}/6$. This procedure uses no chosen point of $K$ and no membership test for $Y$.

The sharper bound on $Y$. For existence only, fix any $\alpha\in K$ and define a bounded coefficient sequence

$$w_0=\alpha/2,\quad w_1=1,\quad w_{2n+2}=2\ell_n+1-2\alpha,\quad w_{2n+3}=2u_n-1-2\alpha.$$

All its coordinates have absolute value at most 1. The functional $g_\alpha(z)=\sum_jw_jz_j$ therefore has norm 1. The identity $z_0=4\sum_{j\geq2}z_j$ on $Y$ shows that $g_\alpha|_Y=f$: the terms involving $\alpha$ cancel. Hence $\|f\|\leq1$, and $f(e_1)=1$ gives equality. The point $\alpha$ is used only to prove the input promise, not in the reduction’s preprocessor.

Theorem 5. Exact recovery of the interval

The admissible values of a norm-at-most-one extension of $f$ at $v_x$ are exactly $K$.

For the reverse inclusion, the functional $g_\alpha$ above extends $f$ and satisfies $g_\alpha(v_x)=\alpha$ for each $\alpha\in K$.

For the forward inclusion, let $g$ be any such extension and put $\alpha=g(v_x)$. Since $Y+\mathbb Rv_x=X$, it is already defined on every unit vector. Using

$$v_{p_n}-v_x=\tfrac12e_{2n+2},\qquad v_{q_n}-v_x=\tfrac12e_{2n+3},$$

its norm bound implies

$$|\ell_n+\tfrac12-\alpha|\leq\tfrac12,\qquad |u_n-\tfrac12-\alpha|\leq\tfrac12.$$

Therefore $\ell_n\leq\alpha\leq u_n$ for every $n$, so $\alpha\in K$.

The preprocessor supplies the fixed $X,Y,v_x$ and the realizer for $f$. A scalar-output oracle returns $\alpha$ directly. A functional-output oracle is postprocessed by evaluating at the fixed vector $v_x$. Every legal answer works. Together with N0002, Corollary 4 and Proposition 5, this gives the ordinary Weihrauch equivalence with $\operatorname{CC}_1$ for this norm-one one-step task.

Corollary 6. The literal exact-norm problems

Retain exactly the input and output conventions of $\operatorname{HBT}^{1}_{\ell^1}$ and $\operatorname{HBT}_{\ell^1}$ from N0001. The same preprocessor, with no extra norm input, proves

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

Indeed Proposition 4 proves that every generated functional satisfies $\|f\|=1$. Every exact-norm output therefore has norm 1 and satisfies Theorem 5. The one-step output domain is all of $\ell^1$ because $Y+\mathbb Rv_x=\ell^1$. In either case, evaluation at the fixed $v_x$ returns a point of the original interval. An exact-norm oracle can be stronger on other inputs without invalidating this reduction on the norm-one inputs actually produced here.

Together with N0002, the equality of degrees established by this construction is for the norm-one restriction, even with the displayed $Y$ and $v_x$ fixed. It is not an equality assertion for all unknown-norm inputs. The norm witness $f(e_1)=\|e_1\|=1$ is precisely what makes this alternative construction insensitive to the missing-norm issue.

Additional consequence of the reconstruction

Not only the ambient space but also the located closed hyperplane $Y$ and the extension vector $v_x$ can be fixed. Only $f$ varies. The upper reduction in N0002 still applies; Theorem 5 gives the lower reduction. This refinement follows from the displayed formulas and is not stated in the supplied draft. It should be checked and attributed as a proposed consequence of the reconstructed argument, not advertised as a verified novelty claim.

Singleton intervals, $K=\{0\}$, $K=\{1\}$ and $K=[0,1]$ all work without a special case or division by an interval width. The point $s$ is essential to the automatic norm-one witness; dropping it would require a fresh normalization argument.

Changelog

2026-09-10 - Version 0.2: add the explicit lower reductions to the literal exact-norm problems; keep the tree/free-space, fixed-hyperplane and functional proofs unchanged. Version 0.1 supplied that reconstruction.