Finite Sequential Word Certificate

Abstract

Complete centered sequential word effects admit dimension-bounded finite certificates.

Theorem 1.1 (Complete finite words have dimension-bounded certificates).

$$\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{centeredHermitianMap}(d,\mathrm{sequentialWordEffect}(J,w)):w:\mathrm{List}(A)\})=\mathrm{traceZeroHermitian}(d)\Rightarrow \\ (\exists W:\mathrm{Finset}(\mathrm{List}(A)),\mathrm{card}(W)\le d^2-1\wedge \\ \mathrm{span}(\mathbb{R},\{\mathrm{centeredHermitianMap}(d,\mathrm{sequentialWordEffect}(J,w)):w\in W\})=\mathrm{traceZeroHermitian}(d))\wedge \\ (\exists n:\mathrm{Nat},n\le d^2-1\wedge \\ \mathrm{span}(\mathbb{R},\{e:\mathrm{traceZeroHermitian}(d)\mid \exists w:\mathrm{List}(A),\mathrm{length}(w)\le n\wedge e=\mathrm{centeredHermitianMap}(d,\mathrm{sequentialWordEffect}(J,w))\})=\mathrm{traceZeroHermitian}(d)). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Each word acts on the identity Hermitian effect through the imported sequentialWordEffect construction. The imported centeredEffect operation removes its scalar trace component on the exact real trace-zero Hermitian carrier.

If the centered effects of all finite words span that carrier, finite-dimensional basis extraction selects a concrete finite word set with at most d squared minus one members and the same span.

For the depth clause, the uncentered bounded-word spans start with the identity line. Once two consecutive stages agree, prefix closure under every instrument generator makes that equality permanent. Their rank can therefore grow strictly at most d squared minus one times, after which canonical centering gives the full bounded centered span.

References

• Truth anchor: D5/S3/Quantum/PredictionDepth/FiniteSequentialWordCertificate.finite_sequential_word_certificate
• Dependency: D5/S3/Quantum/Completion/SequentialWordObservationResidual
• Dependency: D5/S3/Quantum/Fibers/TraceZeroReadoutOrthogonalEquivalence