Finite Sequential Completeness Depth

Abstract

Complete finite sequential word spans reach the full Hermitian carrier at bounded depth.

Theorem 1.1 (Finite-word completeness has a bounded-depth witness).

$$\begin{gathered} \forall d:\mathrm{Nat},\mathrm{NeZero}(d), \\ A:\mathrm{Type}, \\ J:A\to \mathrm{LinearMap}(\mathbb{R},\mathrm{HermitianSpace}(d),\mathrm{HermitianSpace}(d)), \\ \mathrm{span}(\mathbb{R},\{\mathrm{sequentialWordEffect}(J,w):w:\mathrm{List}(A)\})=\mathrm{HermitianSpace}(d)\Rightarrow \\ \exists n:\mathrm{Nat},n\le d^2-1\wedge \\ \mathrm{span}(\mathbb{R},\{e:\mathrm{HermitianSpace}(d)\mid \exists w:\mathrm{List}(A),\mathrm{length}(w)\le n\wedge e=\mathrm{sequentialWordEffect}(J,w)\})=\mathrm{HermitianSpace}(d). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/PredictionDepth/FiniteSequentialCompletenessDepth.finite_sequential_completeness_depth (✓ std3). ∎

Source. Repository-derived.

Commentary.

Each finite word acts on the identity Hermitian effect through the canonical sequentialWordEffect construction on the full real Hermitian carrier.

Canonical trace removal transfers full-span completeness to the real trace-zero carrier, where the frozen finite-word certificate gives the depth bound. Adding back the identity component returns the bounded span to the source’s full Hermitian carrier.

References

• Truth anchor: D5/S3/Quantum/PredictionDepth/FiniteSequentialCompletenessDepth.finite_sequential_completeness_depth
• Dependency: D5/S3/Quantum/PredictionDepth/FiniteSequentialWordCertificate