Quantitative word orthonormal extension
Abstract
A common orthonormal extension has small contraction residuals and bounded short-word coefficients.
Theorem 1.1 (A threshold-stable extension with word certificates).
Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/QuantitativeWordOrthonormalExtension.quantitative_word_orthonormal_extension (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let D, r and M be natural numbers with 2 <= r <= D and M <= D squared. Let 0 < delta < 1. On the complex Euclidean space of dimension D, let A be an arbitrary family of M linear contractions and let eta be an arbitrary orthonormal family of r seed vectors. There is an integer r <= m <= D and one orthonormal family e of length m whose first r vectors are eta. In the display, Fin(k) means the indices 0 through k-1, End over C means complex-linear endomorphisms, and the arrow with subscript zero denotes finitely supported functions. Put W = span(e) and let P be its orthogonal projection; P depends on the same e quantified in the display. Seed indices in e are included by the order-preserving inclusion Fin(r) into Fin(m). Every residual A(a)e(j) - P(A(a)e(j)) has norm at most delta, simultaneously for every a and j.
For this same e, every vector e(j) has a finitely supported complex coefficient family c(j) on pairs (w,b), with w a list of contraction labels and b a seed index. In the display, supp(c(j)) is the finite set of pairs (w,b) with nonzero coefficient, each sum runs over this support, and the absolute-value bars on w denote its length. It satisfies e(j) = sum c(j)(w,b) A(w)eta(b); every supported word has length at most m-r; and sum of the absolute coefficients is at most (D/delta) to the power m-r. The displayed A with word subscript denotes the chronological word operator: the empty word acts as identity, and appending a label a applies A(a) after the existing word. The Lean expression uses the product of the reversed list of endomorphisms.
To extend a current orthonormal family, take a residual whose norm beta exceeds delta and adjoin its normalization. Orthogonality preserves all preceding vectors. The new vector is beta inverse times A(a)e(j) minus its m orthogonal projection terms. Each projection coefficient has modulus at most one. Transporting the existing finite word certificates therefore increases their word lengths by at most one and multiplies their absolute coefficient bound by at most (m+1)/delta <= D/delta. Dimension limits the number of extensions. At termination every residual meets the threshold.
The empty contraction family, full initial dimension r=D, repeated or zero contractions and arbitrarily small positive thresholds are included. No singular-value, conditioning or previously successful extension premise is imposed. This conclusion concerns the finite-dimensional contraction geometry and its coefficients.