Transfinite Hilbert-Basis Residual Tower

Abstract

An initially indexed infinite Hilbert basis determines successor splittings, exact limit stages, full-size proper residuals, and a zero terminal residual.

Theorem 1.1 (Initially indexed bases split every residual stage).

$$\begin{array}{c}\forall K,H,I,b,\\ \mathrm{Hilbert}\left(K,H\right),\mathrm{InfiniteInitialWellOrder}\left(I\right),\mathrm{HilbertBasis}\left(b,I,K,H\right),\\ (\forall i\in I,\mathrm{Residual}\left(b,\mathrm{Iio}\left(i\right)\right)=\mathrm{DirectSum}\left(\mathrm{span}\left(K,b_i\right),\mathrm{Residual}\left(b,\mathrm{Iic}\left(i\right)\right)\right)\wedge \mathrm{Orthogonal}\left(\mathrm{span}\left(K,b_i\right),\mathrm{Residual}\left(b,\mathrm{Iic}\left(i\right)\right)\right))\wedge \\ ((\forall i\in I,\mathrm{Limit}\left(i\right)\Rightarrow \mathrm{Prefix}\left(b,\mathrm{Iio}\left(i\right)\right)=\mathrm{ClosedSup}\left(\mathrm{Prefix}{\left(b,\mathrm{Iio}\left(j\right)\right)}_{j<i}\right)\wedge \mathrm{Residual}\left(b,\mathrm{Iio}\left(i\right)\right)=\mathrm{Inf}\left(\mathrm{Residual}{\left(b,\mathrm{Iio}\left(j\right)\right)}_{j<i}\right))\wedge \\ \mathrm{Prefix}\left(b,I\right)=\mathrm{ClosedSup}\left(\mathrm{Prefix}{\left(b,\mathrm{Iio}\left(j\right)\right)}_{j\in I}\right)\wedge \mathrm{Residual}\left(b,I\right)=\mathrm{Inf}\left(\mathrm{Residual}{\left(b,\mathrm{Iio}\left(j\right)\right)}_{j\in I}\right))\wedge \\ (\forall i\in I,\mathrm{Card}\left(I\setminus \mathrm{Iio}\left(i\right)\right)=\mathrm{Card}\left(I\right)\wedge (\forall j\in I\setminus \mathrm{Iio}\left(i\right),E_i(t_j)=b(epsilo{n}_i(j))))\wedge \\ \mathrm{Residual}\left(b,I\right)=0.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Completion/TransfiniteBasisResidualTower.transfinite_basis_residual_tower (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a Hilbert basis indexed by an infinite initial well-order, the prefix at a set of indices is its closed linear span and the residual is the orthogonal complement of that prefix.

A successor stage splits off the current basis line orthogonally. At a limit index, the prefix is the closed supremum of earlier prefixes and the residual is their intersection.

Every proper initial segment leaves an index complement of the original cardinality. The displayed isometry sends each named tail vector to its reindexed ambient basis vector, while the full-index residual is zero.

References

• Truth anchor: D5/S3/Quantum/Completion/TransfiniteBasisResidualTower.transfinite_basis_residual_tower