InnerProductSpace.toDual (Riesz representation, mathlib) is invoked to produce a vector \(\xi \in M\) satisfying \(f(v) = \langle \xi , v\rangle _M\) for all \(v \in M\). \(\xi \) has classical ontological status: it exists by Riesz but its value is not explicitly computed. This is the formal-register step of the transit: a classical existence result is invoked as a black box. It uses Classical.choice through CompleteSpace and toDual.

\(g := \texttt{innerSL}\, \mathbb {R}\, (\xi : E) : E \to _L[\mathbb {R}] \mathbb {R}\) is defined concretely from \(\xi \) without additional classical machinery. \(g(w) = \langle \xi , w\rangle _E\) for all \(w : E\). Linearity and continuity are automatic from innerSL.

Key factorisation: \(g(\texttt{denseSeq n}) = \langle \xi , \texttt{denseSeq n}\rangle _E = \langle \xi , P_M(\texttt{denseSeq n})\rangle _M = f(P_M(\texttt{denseSeq n}))\), where \(P_M\) is orthogonal projection (available from HasOrthogonalProjection inherited via ClosedSubmodule). Locatedness of \(M\) (dist_computable) makes the projection operationally accessible. fn_computable_everywhere gives computability of \(f\) on all of \(M\), including \(P_M(\texttt{denseSeq n})\). The transit closes: the formal object \(\xi \) is used as an instrument to express the operational result \(g(\texttt{denseSeq n})\) as \(f\) applied to a computable input.

\(g.\texttt{opNorm} = \| \xi \| _E\) via innerSL_apply_norm. \(f.\texttt{opNorm} = \| \xi \| _E\) by le_antisymm: upper bound via Cauchy-Schwarz; lower bound by evaluating \(f.\texttt{le\_ opNorm}\) at \(\xi \). Transitively: \(g.\texttt{opNorm} = f.\texttt{opNorm}\). Computability of \(g.\texttt{opNorm}\) follows from \(f.\texttt{norm\_ computable}\) and the equality.

The Specker obstruction (1949) applies to suprema of bounded monotone computable sequences: such suprema can be non-computable. Path A — invoking classical Hahn-Banach directly — produces an extension abstractly: only an existence result, with no computable witness for \(g(\texttt{denseSeq n})\). This satisfies the formal register but leaves the operational register empty.

Path B (via Riesz) avoids the obstruction structurally: (i) \(\xi \) is a single vector produced by Riesz, not a limit of a monotone sequence; (ii) \(g(\texttt{denseSeq n}) = f(P_M(\texttt{denseSeq n}))\) is a finite-step computation, not a sequence supremum; (iii) \(g.\texttt{opNorm} = \| \xi \| _E\), a single real, not a supremum.

Locatedness (dist_computable) is the key structural ingredient: it makes orthogonal projection applicable at the operational level and enables the factorisation of Step 3. Without locatedness, the projection \(P_M(\texttt{denseSeq n})\) would remain in the formal register.

VR-Audit is an open programme. Audit One (Hahn-Banach for Hilbert spaces via Riesz) establishes the pattern. Future candidates listed in the preprint: Banach-Steinhaus (uniform boundedness), open mapping theorem, closed graph theorem, spectral theorem for self-adjoint compact operators, and Stone-Weierstrass. Each would follow the Mode B schema: classical theorem invoked as formal-register black box; operational output extracted via explicit witnesses and locatedness/computability predicates.

Bishop-Bridges 1985 rebuilds analysis from scratch with constructive proofs. VR-Audit wraps over mathlib’s classical analysis rather than rebuilding it. The operational layer is thinner (predicate restrictions, not new types) and requires fewer proof lines, at the cost of accepting Classical.choice in the formal register.

Reverse mathematics locates each theorem in the subsystem hierarchy (WKL\(_0\), ACA\(_0\), …). VR-Audit does not attempt this classification; it identifies the operational content that can be extracted from a classical theorem at the Classical.choice ceiling, not the minimal axioms needed to prove it.

Pour-El & Richards 1989 and the Weihrauch framework study computability of classical analysis results over abstract computation models. VR-Audit works within Lean 4’s type-theoretic framework: computability is expressed as IsComputableReal predicates rather than oracle Turing machines. The metatheoretic equivalence of these notions is not formalised here.

Computable₂ for \(\mathbb {Q}\) arithmetic operations is absent from mathlib4 (verified by exhaustive search). Lean’s intrinsic totality of alg : ℕ → ℚ and mod : ℕ → ℕ provides algorithmicity at the type level; Turing-machine codings remain metatheoretic. This is the first concrete confirmation in VR-Audit of the architectural principle: operationality is expressed through predicate restrictions, not Lean’s computational machinery. (Parallel to VR-Numbers § IV.1 boundary.)

The field inner_computable : ∀ m n, IsComputableReal (@inner ℝ E _ (denseSeq m) (denseSeq n)) selects, from the classical values provided by InnerProductSpace ℝ E, precisely those pairs for which the inner product is computable. The operational register (computable pairs) lives inside the formal register (full classical InnerProductSpace). This generalises: any classical structure with values in \(\mathbb {R}\) can be wrapped operationally by adding IsComputableReal predicates on selected outputs.

dist_computable is formulated only over denseSeq n (operational witnesses), not arbitrary \(x : E\). This is principled: operational predicates apply to operational objects. Arbitrary \(x : E\) lives in the formal register. Demanding computability on arbitrary points would conflate the registers. The formulation is sufficient for Stage 5 because orthogonal projection is applied precisely to denseSeq points. This pattern — operational predicates only over operational witnesses — generalises to all future VR-Audit work.

The Riesz vector \(\xi \) is a single element, not a limit of a bounded monotone computable sequence. The Specker obstruction (1949) applies to the latter; our construction explicitly avoids it. Locatedness enables orthogonal projection without a Specker-vulnerable supremum. This is the structural reason why Path B (Riesz) is clean where a general Banach Hahn-Banach extension would not be.

In computable analysis (Ishihara 1989), “bounded” (\(\exists C,\; |f(x)| \le C\| x\| \)) and “normable” (exact \(\sup |f(x)|/\| x\| \) computable) are distinct: a functional can be bounded without its norm being computable. norm_computable captures normability; this is required for the norm-preservation clause \(g.\texttt{opNorm} = f.\texttt{opNorm}\) in the main theorem. The distinction collapses classically; it is critical constructively.

The classical extended functional \(g\) is built entirely from operational data: \(\xi \) is the Riesz vector of \(f\); \(g := \texttt{innerSL}\, \mathbb {R}\, (\xi : E)\) is defined concretely. The operational content of \(g\) at denseSeq n comes not from \(g\)’s definition directly but from the factorisation \(g(x) = f(P_M(x))\). This is richer than the standard Mode B schema (“apply classical lemma, prove output operational”): here the classical construction and the operational extraction are interleaved through the projection factorisation.

The Norm (M.toSubmodule →L[ℝ] ℝ) instance does not synthesize at declaration/goal time in this context (mathlib infrastructure gap). Workaround: use f.opNorm (direct field access on ContinuousLinearMap) throughout, and change/show to pass to \(\| \cdot \| \)-based mathlib lemmas inside tactic proofs. This gap is structural (universe/instance unification) and expected in wrapping-style formalisations with multiple unification paths.

The notation ⟪·, ·⟫_ℝ (from open scoped RealInnerProductSpace) does not parse inside class where field type declarations (subscript _ℝ misinterpreted by the parser) nor in \(\exists \)-binder scopes within tactic proofs. Workaround in class fields: use @inner ℝ E _ (explicit arguments). Workaround in binder scopes: use inner ℝ (function form). The notation works normally outside class blocks and binder scopes. This is the second cross-namespace universe issue in VR-Audit (after the OSet.{0} annotation in VR-Forms).

In the main theorem proof, hK_complete (CompleteSpace K) must be introduced via letI (transparent) rather than haveI (opaque) so that tactic-level instance synthesis finds it. Furthermore, @InnerProductSpace.toDual must be called with explicit hK_complete argument because instance synthesis fails to match the unreduced form ↥M.toSubmodule against ↥↑M.toClosedSubmodule. These two obstacles are overcome without new axioms; they reflect the instance-resolution sensitivity of wrapping-style formalisations.

Stage 6 confirms that the operational requirements of OperationalHilbertSpace are achievable on a natural infinite family: \(\mathrm{EuclideanSpace}\, \mathbb {R}\, (\mathrm{Fin}\, n)\) for all \(n : \mathbb {N}\). This is the standard VR-Audit pattern: main theorem in full generality, then at least one explicit instance to show the operationality is inhabited without exotic mathematics.

The use of Classical.choice in VR-Audit is methodologically correct. Classical.choice (AC) lives in the formal register: it produces a classical existence result without a computable witness. The operational register is then extracted via structural arguments (projection factorisation, locatedness, normability) that do not themselves require AC. This is exactly the Mode B pattern of Chapter 8: classical operations with operational witnesses. AC is a formal-register black box; the operational content is the computable output extracted from it.