Finite Detection Dark Space

Abstract

A finite-dimensional repeated-detection dark space is determined after dimension many no-click steps.

Theorem 1.1 (Positive semidefinite dependent block matrices).

$$\forall T:Type,[\mathrm{Fintype}(T)][\mathrm{DecidableEq}(T)]\forall k:T\to Type,[\forall i:T,\mathrm{Fintype}(k(i))][\forall i:T,\mathrm{DecidableEq}(k(i))]\forall M:\forall i:T,\mathrm{Matrix}(k(i))(k(i))(\mathbb{C}),(\forall i:T,\mathrm{Matrix}.\mathrm{PosSemidef}(M(i)))\Rightarrow (\mathrm{Matrix}.\mathrm{PosSemidef}(\mathrm{Matrix}.{\mathrm{blockDiagonal}}^{\prime }(M)))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/FiniteDetectionDarkSpace.positiveBlockDiagonal (✓ std3). ∎

Source. Repository-derived.

Commentary.

A finite dependent block diagonal matrix is positive semidefinite when every diagonal block is positive semidefinite.

Theorem 1.2 (The dark space is a finite survival-defect kernel).

$$\begin{gathered} \forall d:\mathrm{Nat},X:\mathrm{Type},[\mathrm{Fintype}(X)], \\ Q:\mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),L:X\to \mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}), \\ {Q}^{\ast }\cdot Q+\sum _{x\in X}{L}_x^{\ast }\cdot L_x=I_d\Rightarrow \forall psi:\mathrm{Fin}(d)\to \mathbb{C}, \\ (\forall n:\mathrm{Nat},x:X,\mathrm{mulVec}(L_x\cdot Q^n,psi)=0)⟺\mathrm{mulVec}(I_d-{Q^{\ast }}^d\cdot Q^d,psi)=0. \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/FiniteDetectionDarkSpace.dark_space_eq_survival_defect_kernel (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let Q be the no-click operator and let the finite family L_x contain the click operators. Their adjoint products sum with Q^* Q to the identity. The statement also holds in dimension zero, where both sides are trivially true.

The completeness equation telescopes: the defect of the N-step survival operator is the sum, from n = 0 to N - 1 and over all outcomes x, of the Gram operators of L_x Q^n. Positivity therefore identifies its kernel with the common kernel of those event amplitudes.

At N equal to the dimension, Cayley-Hamilton expresses every later power of Q through earlier powers. Hence vanishing of the first dimension many event amplitudes propagates to every time.

References

• Truth anchor: D5/S3/Quantum/Measurement/FiniteDetectionDarkSpace.dark_space_eq_survival_defect_kernel
• Truth anchor: D5/S3/Quantum/Measurement/FiniteDetectionDarkSpace.positiveBlockDiagonal