Hahn-Banach working notes: scope and reading map

Scope and provenance

These are working notes, not an erratum or an independently verified supplement. The mathematical statements below use the explicit conventions in this page and in each individual note. A result already in the paper, or in the earlier literature, is not presented as a new theorem merely because its proof is expanded here.

Representation conventions

All vector spaces and functionals in these notes are real. A fixed computable Banach space comes with its Cauchy representation, computable vector operations and norm, and a fundamental sequence with dense linear span. For varying spaces, all these operations are computed relative to the supplied effective presentation; “uniformly computable” does not mean that arbitrary input names are themselves computable.

A closed linear subspace $A$ is supplied by a sequence of named points whose closure is $A$. A functional is supplied by an evaluation realizer on ambient Cauchy names of points promised to lie in its domain. A program is not required to decide that domain.

The main problems $\operatorname{HBT}_X$ and $\operatorname{HBT}^{1}_X$ use the evaluator-only, positively represented-domain convention of Definition 15 of the versioned paper. Inputs have $0<\|f\|<\infty$; outputs preserve the exact norm, and the exact norm is not an additional input. For $\operatorname{HBT}^{1}_X$, the output is a named functional on $A+\mathbb Rx$, not just its value at $x$. The definition allows $x\in A$.

Within this same framework we explicitly distinguish the following auxiliaries and restrictions.

• $\operatorname{ExtStep}_X(A,f,x)$ is the prescribed-bound scalar helper: $\|f\|\leq1$ is promised, and an admissible value for an extension of norm at most 1 is returned. This is not a renaming of unrestricted $\operatorname{HBT}^{1}_X$.
• $\operatorname{HBT}^{1,=1}_X$ is the restriction of $\operatorname{HBT}^{1}_X$ to inputs with $\|f\|=1$. The analogous restriction of $\operatorname{HBT}_X$ is denoted $\operatorname{HBT}^{=1}_X$, abbreviated $\operatorname{HB}^{=1}_X$ in the existing proofs. These are restrictions with the inherited representation, not new input encodings. The algorithm does not test the promise.
• The known-norm variants take an additional Cauchy name of $r=\|f\|>0$. These do carry genuinely stronger input information. They are mentioned only where that information is supplied or explicitly recovered by an additional noncomputable operation.

A construction can prove that all its generated inputs have norm 1 and feed those same names to an unrestricted exact-norm oracle. No norm field needs to be added to the oracle input. This is why the lower constructions in N0003 and N0006 remain valid for the paper’s literal problem.

If an exact positive $r$ is available, divide by $r$, use the norm-one proofs, and rescale. With only $M\geq\|f\|$, dividing by $M$ is still valid when the subsequent oracle preserves the actual norm $\|f\|/M$. It is not valid to replace that requirement by the weaker bound 1 and then claim exact preservation after rescaling.

N0007 supplies the proposed connection to arbitrary evaluator-only inputs: norm recovery in the limit, followed by the retained interval/loop proofs. It also contains a finite-dimensional obstruction to a universal WKL upper bound under the literal convention. These are follow-up deductions, not claims extracted from the working draft or a formally verified erratum.

Closed interval choice $\operatorname{CC}_1$ takes a nonempty closed interval in $[0,1]$ given negatively and returns a point in it. We use the established equivalence with the strict-sign-change intermediate value problem. We do not silently identify this problem with every possible non-strict endpoint formulation. See Brattka–Le Roux–Miller–Pauly.

Reading map

N0002: Effective one-step intervals expands the analytic interval argument, the enumeration of its complement and the construction of an actual functional realizer. It preserves the draft’s direct certificate method.

N0003: A fixed tree and a fixed hyperplane reconstructs the Lipschitz/free-space route in draft Proposition 7.9. The explicit $\ell^1$ realization closes the effective gap left in that sketch. Its final fixed-hyperplane consequence is an additional deduction of this reconstruction, not a theorem stated in the supplied draft.

N0004: The extension loop expands the stage-data algorithms and the decoding of a whole run. The infinite-loop strategy itself is not an unpublished result.

N0005: Uniform block isometries records the discontinuous-coordinate trap and gives a formula without sign tests, an explicit inverse and the Cauchy-name conversion. The corrected isometry is already part of the paper; the point here is its expanded effective implementation.

N0006: Transport and separator extraction assembles the lower-bound argument, including the original Gherardi–Marcone forcing calculation and a computable finite-precision readout.

N0007: Exact norms and evaluator-only inputs is an additional follow-up note, not an omitted draft section. It gives a norm-information check and an upper bound for the literal input convention without replacing the original geometric or loop arguments.

The logical prerequisite edges are N0002 to N0003, N0002 to N0004, N0004 and N0005 to N0006, and N0002 and N0004 to N0007. This overview is a reading guide, not a premise in those proofs. Its links are recorded as related notes.

What is not being republished as an omitted argument

The paper’s two-dimensional classification and located-subspace section are not missing sections of the supplied draft. They are not reconstructed here as purported unpublished work. Likewise, the classical one-step theorem, the Gherardi–Marcone gadget and the closure of WKL under loops retain their original attribution.

Reuse and corrections

When substantially using a particular argument, cite the relevant note, its version and proposition. Acknowledgements of broader conceptual influence are appreciated. Check the hypotheses and the argument before relying on a working note, and send corrections using the contact link below.

Changelog

2026-09-10 - Version 0.2: retain the paper’s literal problems as the main convention; identify norm-one restrictions and prescribed-bound helpers explicitly; add the follow-up norm-information note. Version 0.1 was the initial proposed web structure.