Uniform block isometries without sign tests

Provenance and normalization

Draft §9.2 contains the block-isometry argument and, on p. 25, a correct warning that its first piecewise formula is discontinuous. The corrected coordinate order is already used in Proposition 25 of the joint paper, v1. This note expands that argument and derives a formula without branching on the sign of a real input.

We retain the draft’s parameter convention $\delta_n=\pm2^{-k}$ at the least occurrence index, so $|\delta_n|\leq1$. The paper instead uses $\pm2^{-k-1}$. These are different numerical conventions. The proof below is valid on the entire interval $[-1,1]$, and hence also for the paper’s parameters. No global quotient $(1-\delta)/(1+\delta)$ is formed at $\delta=-1$.

Proposition 1. Uniform real parameters

Let $p,q:\mathbb N\to\mathbb N$ enumerate disjoint ranges. Define $\delta_n=2^{-k}$ if $k$ is the least index with $p(k)=n$, define $\delta_n=-2^{-k}$ for the least $q$ occurrence, and set it to zero when neither occurs.

The real number $\delta_n$ is computable uniformly relative to $(p,q,n)$. To obtain error less than $2^{-m}$, inspect both input sequences through index $m$. If $n$ occurs, its signed value is determined exactly using the least index. Otherwise output zero: any later value has magnitude at most $2^{-(m+1)}$.

This does not compute the sign or decide whether the real is zero. The least-index notation is ordinary minimization, not an additional parameter. Duplicate enumeration values do not affect the construction.

The block norms

For $\delta\in[-1,1]$ let

$$\| (\alpha,\beta)\|_\delta=\begin{cases} \max\left(\left|\frac{1-\delta}{1+\delta}\alpha+\beta\right|,|\alpha-\beta|\right),&\delta>0,\\ \max\left(|\alpha+\beta|,\left|\frac{1+\delta}{1-\delta}\alpha-\beta\right|\right),&\delta<0,\\ \max(|\alpha+\beta|,|\alpha-\beta|),&\delta=0. \end{cases}$$

Only the respective safe denominators occur in this case description. The uniformly computable implementation will be the single formula below, not a procedure that first decides which case holds.

Proposition 2. A branch-free isometry and inverse

Define

$$\boxed{\Theta_\delta(\alpha,\beta)=\left(\beta-\frac{\delta\alpha}{1+|\delta|},\frac{\alpha}{1+|\delta|}\right).}$$

Then

$$\|\Theta_\delta(\alpha,\beta)\|_1=\|(\alpha,\beta)\|_\delta,$$

and

$$\boxed{\Theta_\delta^{-1}(u,v)=\bigl((1+|\delta|)v,\ u+\delta v\bigr).}$$

Both maps are computable uniformly in the real parameter $\delta$ and their vector input.

Proof. Let $S(u,v)=((u-v)/2,(u+v)/2)$. The elementary identity $|u-v|+|u+v|=2\max(|u|,|v|)$ shows that $S$ is an isometry from $\ell^\infty_2$ to $\ell^1_2$.

When $\delta>0$, composing $S$ with

$$T_\delta(\alpha,\beta)=\left(\frac{1-\delta}{1+\delta}\alpha+\beta,\alpha-\beta\right)$$

gives the boxed formula. When $\delta<0$, use the corrected coordinate order

$$T_\delta(\alpha,\beta)=\left(\alpha+\beta,\frac{1+\delta}{1-\delta}\alpha-\beta\right).$$

The same simplification gives the boxed formula. At zero it gives $\Theta_0(\alpha,\beta)=(\beta,\alpha)$, agreeing with $S(\alpha+\beta,\alpha-\beta)$. The norm identity follows in every case, and substitution verifies the inverse.

The operations of absolute value, arithmetic and division by the number $1+|\delta|\geq1$ are computable on Cauchy names. This is the effective argument: continuity of a piecewise formula alone would not establish computability.

The discontinued first formula

The draft’s original negative branch placed the two components of $T_\delta$ in the opposite order. At $(\alpha,\beta)=(0,1)$, that branch gives $S(-1,1)=(-1,0)$ for every negative $\delta$, whereas its value at zero is $S(1,-1)=(1,0)$. It is therefore genuinely discontinuous in the parameter.

The branch-free formula gives $\Theta_\delta(0,1)=(1,0)$ for all $\delta$. It implements the corrected order and should replace the old order everywhere, including the auxiliary $T_n$ in the subsequent proof. A marginal proposed correction is not enough if a later lemma still uses the old definition.

Proposition 3. The weighted global isometry

Let $w_n=2^{-n-1}$ and

$$X_{p,q}=\left\{x=(x_n)_{n\geq0}:x_n\in\mathbb R^2,\quad \|x\|_{p,q}=\sum_n w_n\|x_n\|_{\delta_n}<\infty\right\}.$$

Define $J_{p,q}:X_{p,q}\to\ell^1(\mathbb N)$ by

$$J_{p,q}(x)_{2n}=w_n\left(\beta_n-\frac{\delta_n\alpha_n}{1+|\delta_n|}\right),\qquad J_{p,q}(x)_{2n+1}=w_n\frac{\alpha_n}{1+|\delta_n|},$$

where $x_n=(\alpha_n,\beta_n)$. It is a surjective linear isometry, and it and its inverse are computable uniformly relative to $(p,q)$.

Norm and surjectivity. The block identity gives

$$\|J_{p,q}x\|_1=\sum_nw_n\|\Theta_{\delta_n}x_n\|_1=\|x\|_{p,q}.$$

For $z\in\ell^1$, set

$$\alpha_n=w_n^{-1}(1+|\delta_n|)z_{2n+1},\qquad \beta_n=w_n^{-1}(z_{2n}+\delta_nz_{2n+1}).$$

The block inverse and norm identity imply that these coordinates define an element of $X_{p,q}$ with norm $\|z\|_1$, and $J_{p,q}x=z$. Although $w_n^{-1}$ grows, the weighted target norm exactly compensates for it. Coordinatewise inversion alone would not have been a proof that the infinite vector belongs to the source space; the norm identity supplies that proof.

Cauchy names. Use the dense finite rational block vectors in $X_{p,q}$ and finite rational sequences in $\ell^1$. Computing the image of a finite rational vector produces finitely many computable real coordinates, which need not be rational. To produce a rational Cauchy approximant for $Jx$ with error less than $2^{-k}$, take an input rational approximant $u$ to $x$ with error at most $2^{-(k+2)}$, compute $Ju$ and approximate its finitely many coordinates by rationals with total $\ell^1$ error less than $2^{-(k+2)}$. The isometry bounds the remaining error, giving less than $2^{-k}$ in total.

Apply the same procedure to the inverse. Finite-coordinate approximation in its target norm is effective, for example using $\|(\alpha,\beta)\|_\delta\leq|\alpha|+|\beta|$, which follows because both coordinate unit vectors have norm 1. This finite re-approximation step turns the informal instruction “map the Cauchy sequence” into an actual name conversion.

A useful fixed readout vector

Let $z_n$ be the vector with $(0,1)$ in block $n$ and zero elsewhere. The branch-free formula gives

$$J_{p,q}(z_n)=2^{-n-1}e_{2n}.$$

This image is independent of the input instance. N0006 uses it to extract a separator without needing the original $(p,q)$ in the postprocessor.

Attribution and changelog

The varying block-space gadget originates in Gherardi and Marcone, How incomputable is the separable Hahn-Banach theorem?, Theorem 8.12. The source for the draft’s isometry and correction is its §§9.1–9.2; compare Proposition 25 of the joint paper. The closed-form simplification and explicit Cauchy-name accounting are additions to this exposition, not priority claims.

2026-09-10 - Version 0.1: branch-free isometries, inverses and name conversions.