The Eventual-Click Doob Instrument

Abstract

The support Doob transform realizes finite click branches conditioned on eventual detection.

Theorem 1.1 (Conditioning on an eventual click).

$$\begin{gathered} \forall d\in \mathbb{N},alpha:\mathrm{Type},xi:\mathrm{Type},beta:\mathrm{Type}, \\ [\mathrm{Fintype}(alpha)],[\mathrm{Fintype}(xi)],[\mathrm{Fintype}(beta)], \\ Q:alpha\to \mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),L:xi\to beta\to \mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),F:\mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}), \\ (\sum _{a\in alpha}({Q(a)}^{\ast })(Q(a))+\sum _{x\in xi}\sum _{b\in beta}({L(x,b)}^{\ast })(L(x,b))=I)\Rightarrow \\ (\underset{n\to \infty }{\lim }\mathrm{survival}(Q,n)=F)\Rightarrow \\ \mathrm{let}N:=(X\mapsto \sum _{a\in alpha}(Q(a))(X)({Q(a)}^{\ast })) \\ \mathrm{let}C:=(x,X\mapsto \sum _{b\in beta}(L(x,b))(X)({L(x,b)}^{\ast })) \\ \mathrm{let}R:=(I-F) \\ \mathrm{let}P:=\mathrm{spectralSupport}(R) \\ \mathrm{let}G:=\mathrm{cfc}((t\mapsto \mathrm{sqrt}(t)),R) \\ \mathrm{let}Gplus:=\mathrm{spectralInverseSqrt}(R) \\ \mathrm{let}Ntilde:=(X\mapsto (G)(N((Gplus)(X)(Gplus)))(G)) \\ \mathrm{let}Ctilde:=(x,X\mapsto C(x,(Gplus)(X)(Gplus))) \\ (R=\mathrm{noClickDual}(Q,R)+\sum _{x\in xi}\mathrm{noClickDual}(L(x),I))\wedge \\ (\forall a\in alpha,(P)(Q(a))((I-P))=0)\wedge \\ (\forall x\in xi,\forall b\in beta,(L(x,b))((I-P))=0)\wedge \\ (\forall H:\mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),(H=(P)(H)(P))\Rightarrow (\mathrm{noClickDual}(Q,H)=(P)(\mathrm{noClickDual}(Q,H))(P)))\wedge \\ (\forall x\in xi,\forall Z:\mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),\mathrm{noClickDual}(L(x),Z)=(P)(\mathrm{noClickDual}(L(x),Z))(P))\wedge \\ ((Gplus)(G)=P)\wedge \\ ((G)(Gplus)=P)\wedge \\ ((P)(G)=G)\wedge \\ (\forall X:\mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),\mathrm{Ntilde}(X)=\sum _{a\in alpha}((G)(Q(a))(Gplus))(X)({(G)(Q(a))(Gplus)}^{\ast }))\wedge \\ (\forall x\in xi,\forall X:\mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),\mathrm{Ctilde}(x,X)=\sum _{b\in beta}((L(x,b))(Gplus))(X)({(L(x,b))(Gplus)}^{\ast }))\wedge \\ (\sum _{a\in alpha}({(G)(Q(a))(Gplus)}^{\ast })(P)((G)(Q(a))(Gplus))+\sum _{x\in xi}\sum _{b\in beta}({(L(x,b))(Gplus)}^{\ast })((L(x,b))(Gplus))=P)\wedge \\ (\forall X:\mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),\mathrm{Ntilde}((G)(X)(G))=(G)(N(X))(G))\wedge \\ (\forall x\in xi,\forall X:\mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),\mathrm{Ctilde}(x,(G)(X)(G))=C(x,X))\wedge \\ (\forall \rho :\mathrm{DensityState}(\mathrm{Fin}(d)),\forall n\in \mathbb{N},(1\le n)\Rightarrow \mathrm{let}rhoMatrix:=\mathrm{ofMatrixSymm}(\mathrm{val}(\rho )) \\ \mathrm{let}r:=\mathrm{Re}\mathrm{Tr}((rhoMatrix)(R)) \\ (0<r)\Rightarrow (\forall x\in xi,\mathrm{let}original:=C(x,N^{(n-1)}(rhoMatrix)) \\ \mathrm{let}conditioned:=\mathrm{Ctilde}(x,{Ntilde}^{(n-1)}(((r^{-1}))((G)(rhoMatrix)(G)))) \\ (conditioned=((r^{-1}))(original))\wedge \\ (\mathrm{Tr}(conditioned)=\frac{\mathrm{Tr}(original)}{r})\wedge \\ ((\mathrm{Tr}(original)\ne 0)\Rightarrow ((\mathrm{Tr}(conditioned)\ne 0)\wedge \\ ((({\mathrm{Tr}(conditioned)}^{-1}))(conditioned)=(({\mathrm{Tr}(original)}^{-1}))(original)))))). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Let Q be the no-click Kraus family and L the click Kraus family of a complete finite-dimensional instrument. If the survival effects converge to F, then the residual effect R = I - F satisfies the one-step balance law. Every click Kraus operator vanishes on the orthogonal complement of the support P of R, and P Q (I - P) = 0 for every no-click Kraus operator. Consequently the no-click pullback maps operators supported on P to operators supported on P, and every click pullback is supported on P.

The square root G of R and its support pseudo-inverse Gplus obey Gplus G = G Gplus = P and P G = G. Conjugating the no-click channel and pulling back the click maps by Gplus gives the displayed Kraus families, completeness on P, and both intertwining identities.

For a density state with positive residual weight r, the transformed branch at every positive time equals the original click branch divided by r. Its trace has the same likelihood-ratio form, and whenever that trace is nonzero the two normalized terminal states coincide.

References

• Truth anchor: D5/S3/Quantum/Measurement/EventualClickDoobInstrument.eventual_click_doob_instrument
• Dependency: D5/S3/Quantum/Foundation/FiniteKrausChannel
• Dependency: D5/S3/Quantum/Measurement/GeneralInstrumentResidualTailContraction
• Dependency: D5/S3/Quantum/Recovery/SpectralTransposeRecovery