Branch-Conditioned Trace Distance

Abstract

A trace-nonincreasing finite Kraus branch contracts trace distance after weighting by its probability.

Theorem 1.1 (Conditioning is stable above the branch-probability floor).

$$\begin{gathered} \forall d:\mathrm{Nat},iota:\mathrm{Type},[\mathrm{Fintype}(iota)], \\ rho:\mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),sigma:\mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}),K:iota\to \mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C}), \\ \mathrm{PosSemidef}(rho)\wedge \left(\mathrm{Tr}(rho)=1\wedge \left(\mathrm{PosSemidef}(sigma)\wedge \mathrm{Tr}(sigma)=1\right)\right), \\ \sum _{i\in iota}{K_i}^{\ast }\cdot K_i\le I_d\Rightarrow \mathrm{let}B:\mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C})=\sum _{i\in iota}{K_i}^{\ast }\cdot K_i, \\ Phi:\mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C})\to \mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C})=X\mapsto \sum _{i\in iota}{K}_i\cdot X\cdot {K_i}^{\ast }, \\ p:\mathbb{R}=\mathrm{Re}(\mathrm{Tr}(rho\cdot B)),q:\mathbb{R}=\mathrm{Re}(\mathrm{Tr}(sigma\cdot B)), \\ D:\mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C})\to \mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C})\to \mathbb{R}=X,Y\mapsto \frac{\mathrm{traceNorm}(X-Y)}{2}; \\ |p-q|\le D(rho,sigma)\wedge \left(\left(\left(0<p\wedge 0<q\right)\Rightarrow \max (p,q)\cdot D(\frac{1}{p}\cdot Phi(rho),\frac{1}{q}\cdot Phi(sigma))\le D(rho,sigma)\right)\wedge \left(\forall pStar\in \mathbb{R},epsilon\in \mathbb{R},\left(0<pStar\wedge \left(pStar\le p\wedge \left(D(rho,sigma)\le epsilon\wedge epsilon<pStar\right)\right)\right)\Rightarrow \left(0<q\wedge D(\frac{1}{p}\cdot Phi(rho),\frac{1}{q}\cdot Phi(sigma))\le \frac{epsilon}{pStar}\right)\right)\right). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Let rho and sigma be positive semidefinite matrices of trace one. A finite Kraus family defines a completely positive branch whose effect is bounded by the identity, and p and q are its probabilities on the two states.

The traceless Hermitian state difference splits into positive and negative parts of equal trace. Positivity of the branch and its complementary failure weight bounds both the probability change and the surviving trace-norm change by the original Jordan mass.

Normalizing the two branch outputs introduces an inverse probability. Weighting by the larger branch probability removes this denominator. A positive probability floor therefore turns an input error epsilon into conditioned error at most epsilon divided by that floor.

References

• Truth anchor: D5/S3/Quantum/Measurement/BranchConditionedTraceDistance.branch_conditioned_trace_distance
• Dependency: D5/S3/Quantum/Foundation/FiniteTraceDistance