Rare-Branch Conditional Error Sharpness

Abstract

An arbitrarily small initial state error can reach maximal error after conditioning on a rare branch.

Theorem 1.1 (A rare branch reaches maximal conditional error).

$$\left(\forall epsilon\in \mathbb{R},\left(0<epsilon\wedge epsilon<1\right)\Rightarrow \left(\exists rho\in \mathrm{DensityState}(\mathrm{Fin}(3)),\exists sigma\in \mathrm{DensityState}(\mathrm{Fin}(3)),\exists P\in \mathrm{Matrix}(\mathrm{Fin}(3),\mathrm{Fin}(3),\mathbb{C}),\exists K\in \mathrm{Matrix}(\mathrm{Fin}(3),\mathrm{Fin}(3),\mathbb{C}),\mathrm{matrix}(rho)=\mathrm{diagonalState}((1-epsilon,epsilon,0))\wedge \left(\mathrm{matrix}(sigma)=\mathrm{diagonalState}((1-epsilon,0,epsilon))\wedge \left(P=\mathrm{basisProjector}(1)+\mathrm{basisProjector}(2)\wedge \left(K=\mathrm{basisProjector}(0)\wedge \left(P^{\ast }\cdot P+K^{\ast }\cdot K=1\wedge \left(P^{\ast }\cdot P\le 1\wedge \left(\mathrm{traceDistance}(rho,sigma)=epsilon\wedge \left(\mathrm{ReTr}(\mathrm{matrix}(rho)\cdot P^{\ast }\cdot P)=epsilon\wedge \left(\mathrm{ReTr}(\mathrm{matrix}(sigma)\cdot P^{\ast }\cdot P)=epsilon\wedge \left(1/epsilon\cdot P\cdot \mathrm{matrix}(rho)\cdot P^{\ast }=\mathrm{basisProjector}(1)\wedge \left(1/epsilon\cdot P\cdot \mathrm{matrix}(sigma)\cdot P^{\ast }=\mathrm{basisProjector}(2)\wedge \left(\mathrm{traceNorm}((\mathrm{basisProjector}(1)-\mathrm{basisProjector}(2)))/2=1\wedge \max (epsilon,epsilon)\cdot (\mathrm{traceNorm}((1/epsilon\cdot P\cdot \mathrm{matrix}(rho)\cdot P^{\ast }-1/epsilon\cdot P\cdot \mathrm{matrix}(sigma)\cdot P^{\ast }))/2)=\mathrm{traceDistance}(rho,sigma)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\wedge \left(\neg \left(\exists f\in (\mathbb{R})\to \mathbb{R},\mathrm{Tendsto}(f,\mathrm{nhdsGT}(0),\mathrm{nhds}(0))\wedge \left(\forall rho\in \mathrm{DensityState}(\mathrm{Fin}(3)),\forall sigma\in \mathrm{DensityState}(\mathrm{Fin}(3)),\forall P\in \mathrm{Matrix}(\mathrm{Fin}(3),\mathrm{Fin}(3),\mathbb{C}),\left(P^{\ast }\cdot P\le 1\wedge \left(0<\mathrm{ReTr}(\mathrm{matrix}(rho)\cdot P^{\ast }\cdot P)\wedge 0<\mathrm{ReTr}(\mathrm{matrix}(sigma)\cdot P^{\ast }\cdot P)\right)\right)\Rightarrow \mathrm{traceNorm}((1/\mathrm{ReTr}(\mathrm{matrix}(rho)\cdot P^{\ast }\cdot P)\cdot P\cdot \mathrm{matrix}(rho)\cdot P^{\ast }-1/\mathrm{ReTr}(\mathrm{matrix}(sigma)\cdot P^{\ast }\cdot P)\cdot P\cdot \mathrm{matrix}(sigma)\cdot P^{\ast }))/2\le f(\mathrm{traceDistance}(rho,sigma))\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

For every positive epsilon below one, the displayed diagonal density states have trace distance epsilon while the same single-Kraus branch has equal probability epsilon on both states.

After normalization, the two branch outputs are orthogonal rank-one projectors, so their trace distance is one and the weighted sharpness identity is attained.

The construction also rules out any uniform conditional-error bound whose value tends to zero with the initial trace distance.

References

• Truth anchor: D5/S3/Quantum/Measurement/RareBranchConditionalErrorSharpness.rare_branch_conditional_error_sharpness
• Dependency: D5/S3/Quantum/Decoherence/ProjectedUnistochasticDynamics
• Dependency: D5/S3/Quantum/Foundation/FiniteTraceDistance