A Permanent Dark Effect Need Not Be a Projection

Abstract

A permanent no-click effect can retain fractional weight outside its certain dark directions.

Theorem 1.1 (A two-dimensional non-projective dark effect).

$$\forall a\in \mathbb{R},(0<a)\Rightarrow ((a<1)\Rightarrow (\exists Q\in (\mathrm{Fin}(2))\to \mathrm{Matrix}(\mathrm{Fin}(2),\mathrm{Fin}(2),\mathbb{C}),\exists L\in (\mathrm{Fin}(1))\to \mathrm{Matrix}(\mathrm{Fin}(2),\mathrm{Fin}(2),\mathbb{C}),\exists F\in \mathrm{Matrix}(\mathrm{Fin}(2),\mathrm{Fin}(2),\mathbb{C}),(Q(0)=\mathrm{basisProjector}(0))\wedge \left((Q(1)=\mathrm{single}(0,1,\mathrm{sqrt}(a)))\wedge \left((L(0)=\mathrm{sqrt}((1-a))\cdot \mathrm{basisProjector}(1))\wedge \left((\sum _{i\in \mathrm{Fin}(2)}{Q(i)}^{\ast }\cdot Q(i)+\sum _{i\in \mathrm{Fin}(1)}{L(i)}^{\ast }\cdot L(i)=1)\wedge \left((\forall X\in \mathrm{Matrix}(\mathrm{Fin}(2),\mathrm{Fin}(2),\mathbb{C}),\mathrm{noClickDual}(Q,X)=X_{00}\cdot F)\wedge \left((\forall N\in \mathrm{Nat},(1\le N)\Rightarrow (\mathrm{survival}(Q,N)=F))\wedge \left((\mathrm{Tendsto}(\mathrm{survival}(Q),atTop,\mathrm{nhds}(F)))\wedge \left((F=\mathrm{basisProjector}(0)+a\cdot \mathrm{basisProjector}(1))\wedge \left((F\cdot F\ne F)\wedge \left((\forall v\in (\mathrm{Fin}(2))\to \mathbb{C},(\mathrm{dotProduct}(\mathrm{star}(v),v)=1)\Rightarrow ((\mathrm{dotProduct}(\mathrm{star}(v),\mathrm{mulVec}(F,v))=1)\iff (v(1)=0)))\wedge \left((\mathrm{trace}(\mathrm{basisProjector}(1)\cdot F)=a)\wedge \left((\mathrm{trace}(\mathrm{basisProjector}(1)\cdot {L(0)}^{\ast }\cdot L(0))=(1-a))\wedge (\mathrm{trace}(\mathrm{basisProjector}(1)\cdot \mathrm{basisProjector}(0))=0)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)))$$

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

Source. Repository-derived.

Commentary.

For each real a strictly between zero and one, two no-click Kraus operators and one click Kraus operator satisfy the completeness equation. The dual no-click map depends only on the upper-left entry and the survival effect is constant after the first step.

The limiting effect has diagonal entries one and a, so it is not idempotent. A unit vector has expectation one exactly when its second coordinate vanishes.

The second basis state has permanent no-click probability a even though its weight on the certain dark direction is zero.

References

• Truth anchor: D5/S3/Quantum/Measurement/NonProjectiveDarkEffect.non_projective_dark_effect
• Dependency: D5/S3/Quantum/Decoherence/ProjectedUnistochasticDynamics
• Dependency: D5/S3/Quantum/Measurement/GeneralInstrumentSurvivalLimit