Finite Detection Tail Bound
Abstract
Finite-dimensional repeated detection has a geometric survival tail above its dark subspace.
Theorem 1.1 (Survival beyond the dark weight has a finite geometric tail).
Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/FiniteDetectionTailBound.finite_detection_tail_bound (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let Q be the no-click operator, let L_x be the finite family of click operators, and let P be the orthogonal projection onto the vectors that never click. Completeness forces survival on the orthogonal complement of that dark space to contract uniformly within one dimension block.
There is a real gap g strictly between zero and one inclusive. At every block endpoint, the survival operator above P is positive and is bounded in the Loewner order by the corresponding geometric multiple of I-P.
For every positive semidefinite trace-one matrix supported orthogonally to the dark space, the real survival probabilities form a summable sequence. Their total is at most the dimension divided by g.