Single-Kraus Survival Limit

Abstract

For a complete finite measurement with one no-click operator, the survival effects converge to the orthogonal projection onto the vectors that no click can ever detect.

Definition 1.1 (The indefinitely undetected subspace).

$$\begin{gathered} \forall d:\mathbb{N},X:\mathrm{Type}, \\ Q:\mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),L:X\to \mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),\mathrm{darkSpace}(Q,L)=\mathrm{iInter}(n\in \mathbb{N},x\in X,\ker (L_x\cdot Q^n)). \end{gathered}$$

Formalization. D5/S3/Quantum/Measurement/FiniteDetectionSurvivalLimit.darkSpace (✓ std3).

Source. Repository-derived.

Commentary.

The dark space consists of the vectors annihilated by every click operator after every finite number of no-click steps.

Definition 1.2 (The orthogonal dark-space projection).

$$\begin{gathered} \forall d:\mathbb{N},X:\mathrm{Type}, \\ Q:\mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),L:X\to \mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),\mathrm{darkProjection}(Q,L)=\mathrm{matrix}(\mathrm{starProjection}(\mathrm{darkSpace}(Q,L))). \end{gathered}$$

Formalization. D5/S3/Quantum/Measurement/FiniteDetectionSurvivalLimit.darkProjection (✓ std3).

Source. Repository-derived.

Commentary.

The dark projection is the matrix of the orthogonal projection onto the dark space.

Theorem 1.3 (Dark-complement survival contracts geometrically by dimension blocks).

$$\begin{gathered} \forall d:\mathbb{N},X:\mathrm{Type}, \\ Q:\mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),L:X\to \mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),[\mathrm{Fintype}(X)], \\ (Q^{\ast }\cdot Q+\sum _{x\in X}{L}_x^{\ast }\cdot L_x=I_d\wedge d\ne 0)\Rightarrow \\ \exists g\in \mathbb{R},c\in \mathbb{N}\to \mathbb{R},\left(\left(\left(\left(\left(\left(\left(\left(\left(\left(\left(\left(\left(\left(0<g\wedge g\le 1\right)\wedge (\forall N\in \mathbb{N},0\le c(N))\right)\wedge (\forall N\in \mathbb{N},c(N)\le 1)\right)\wedge (\forall N\in \mathbb{N},c(N+d)\le (1-g)\cdot c(N))\right)\wedge (\forall N\in \mathbb{N},\mathrm{darkProjection}(Q,L)\le (Q^{\ast }{)}^N\cdot Q^N)\right)\wedge (\forall N\in \mathbb{N},(Q^{\ast }{)}^N\cdot Q^N-\mathrm{darkProjection}(Q,L)=(I_d-\mathrm{darkProjection}(Q,L))\cdot (Q^{\ast }{)}^N\cdot Q^N\cdot (I_d-\mathrm{darkProjection}(Q,L)))\right)\wedge 0\le (I_d-\mathrm{darkProjection}(Q,L))\right)\wedge (\forall N\in \mathbb{N},(Q^{\ast }{)}^N\cdot Q^N-\mathrm{darkProjection}(Q,L)\le \mathrm{smul}(c(N),(I_d-\mathrm{darkProjection}(Q,L))))\right)\wedge (\forall N\in \mathbb{N},\Vert (Q^{\ast }{)}^N\cdot Q^N-\mathrm{darkProjection}(Q,L)\Vert \le c(N))\right)\wedge 1-g=c(d)\right)\wedge (Q^{\ast }{)}^d\cdot Q^d-\mathrm{darkProjection}(Q,L)\le \mathrm{smul}((1-g),(I_d-\mathrm{darkProjection}(Q,L)))\right)\wedge (\forall n\in \mathbb{N},k\in \mathbb{N},c(n+k\cdot d)\le (1-g{)}^k)\right)\wedge (\forall N\in \mathbb{N},c(N)\le (1-g{)}^{\mathrm{div}(N,d)})\right)\wedge (\forall n\in \mathbb{N},k\in \mathbb{N},(Q^{\ast }{)}^{n+k\cdot d}\cdot Q^{n+k\cdot d}-\mathrm{darkProjection}(Q,L)\le \mathrm{smul}((1-g{)}^k,(I_d-\mathrm{darkProjection}(Q,L))))\right)\wedge (\forall N\in \mathbb{N},(Q^{\ast }{)}^N\cdot Q^N-\mathrm{darkProjection}(Q,L)\le \mathrm{smul}((1-g{)}^{\mathrm{div}(N,d)},(I_d-\mathrm{darkProjection}(Q,L)))). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Let Q be the no-click operator and L_x the finite family of click operators. Their adjoint products sum with Q^* Q to the identity. The survival defect above the dark projection is positive, factors through the dark complement, and is controlled by squared norms of restricted powers.

Compactness of the unit sphere in the finite-dimensional dark complement turns strict decay after d steps into a uniform positive gap g. Iterating that block contraction bounds the defect at n+kd by (1-g)^k, and the quotient-remainder decomposition gives the corresponding bound at every N.

Theorem 1.4 (Survival converges exactly to the dark projection).

$$\begin{gathered} \forall d:\mathbb{N},X:\mathrm{Type}, \\ Q:\mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),L:X\to \mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),[\mathrm{Fintype}(X)], \\ {Q}^{\ast }\cdot Q+\sum _{x\in X}{L}_x^{\ast }\cdot L_x=I_d\Rightarrow \\ \underset{N\to \infty }{\lim }{Q^{\ast }}^N\cdot Q^N=\mathrm{darkProjection}(Q,L)\wedge \forall rho:\mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),\underset{N\to \infty }{\lim }\mathrm{Tr}(rho\cdot {Q^{\ast }}^N\cdot Q^N)=\mathrm{Tr}(rho\cdot \mathrm{darkProjection}(Q,L)). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Let Q be the no-click operator and let the finite family L_x contain the click operators. Assume that their adjoint products sum with Q^* Q to the identity. The dark space is invariant under Q. On it, Q^*Q is the identity, and finite dimensionality makes the restriction of Q surjective. Consequently the orthogonal complement of the dark space is also invariant under Q.

The dimension-step survival defect has the dark space as its kernel. Positivity therefore makes the dimension-step restriction a strict contraction on the orthogonal complement. Compactness of its unit sphere upgrades pointwise strictness to a uniform contraction, whose powers decay geometrically.

Survival is the identity on the dark space and tends to zero on its orthogonal complement. Hence the survival matrices converge to the orthogonal dark-space projection. Multiplication by any matrix rho followed by the trace is continuous, which gives the trace limit. Dimension zero is included.

References

• Truth anchor: D5/S3/Quantum/Measurement/FiniteDetectionSurvivalLimit.darkProjection
• Truth anchor: D5/S3/Quantum/Measurement/FiniteDetectionSurvivalLimit.darkSpace
• Truth anchor: D5/S3/Quantum/Measurement/FiniteDetectionSurvivalLimit.dark_block_contraction
• Truth anchor: D5/S3/Quantum/Measurement/FiniteDetectionSurvivalLimit.finite_detection_survival_limit
• Dependency: D5/S3/ObserverMemory/Dynamics/MaximalUnobservableSubspace
• Dependency: D5/S3/ObserverMemory/Dynamics/ResidualKernelInvariance
• Dependency: D5/S3/Quantum/Measurement/FiniteDetectionDarkSpace