Exact Conditional Preparation Cost

Abstract

Exact universal conditional preparation is a scalar square-root filter, with optimal worst-case success equal to the spectral endpoint ratio.

Definition 1.1 (Exact conditional preparation contract).

$$\begin{gathered} \forall rho:\mathrm{Matrix}(Iota,Iota,\mathbb{C}),((\mathrm{PosSemidef}(rho))\wedge \\ (\mathrm{Tr}(rho)=1))\Rightarrow ((0<\mathrm{Re}(\mathrm{Tr}(\mathrm{ofKraus}(K,K,rho))))\wedge \\ (\mathrm{ofKraus}(K,K,rho)=\mathrm{Tr}(\mathrm{ofKraus}(K,K,rho))/\mathrm{Tr}(R\cdot rho)\cdot \mathrm{sqrt}(R)\cdot rho\cdot \mathrm{sqrt}(R))\wedge \\ (\mathrm{TraceNonincreasing}(K))) \end{gathered}$$

Formalization. D5/S3/Quantum/Measurement/ExactConditionalPreparationCost.ExactPreparationContract (✓ std3).

Source. Repository-derived.

Commentary.

On every positive trace-one input, the output has positive real trace and is the normalized positive-square-root sandwich associated with the effect; the Kraus family is trace-nonincreasing.

Definition 1.2 (Trace-nonincreasing Kraus family).

$$\mathrm{PosSemidef}(I-\sum _{j\in \mathrm{Fin}(m)}\mathrm{star}(K(j))\cdot K(j))$$

Formalization. D5/S3/Quantum/Measurement/ExactConditionalPreparationCost.TraceNonincreasing (✓ std3).

Source. Repository-derived.

Commentary.

A Kraus family is trace-nonincreasing when the identity minus its total effect is positive semidefinite.

Definition 1.3 (Least eigenvalue).

$$\mathrm{leastEigenvalue}(R)=\inf (\mathrm{eigenvalues}(R))$$

Formalization. D5/S3/Quantum/Measurement/ExactConditionalPreparationCost.leastEigenvalue (✓ std3).

Source. Repository-derived.

Commentary.

The least eigenvalue is the infimum of the finite Hermitian eigenvalue family.

Definition 1.4 (Greatest eigenvalue).

$$\mathrm{greatestEigenvalue}(R)=\sup (\mathrm{eigenvalues}(R))$$

Formalization. D5/S3/Quantum/Measurement/ExactConditionalPreparationCost.greatestEigenvalue (✓ std3).

Source. Repository-derived.

Commentary.

The greatest eigenvalue is the supremum of the finite Hermitian eigenvalue family.

Theorem 1.5 (Rigidity, optimal cost, and determinism).

$$\begin{gathered} \forall Iota:\mathrm{Type},\mathrm{Fintype}(Iota),\mathrm{DecidableEq}(Iota),\mathrm{Nonempty}(Iota), \\ R:\mathrm{Matrix}(Iota,Iota,\mathbb{C}),\mathrm{PosDef}(R), \\ (\forall m:\mathbb{N},\forall K:(\mathrm{Fin}(m))\to \mathrm{Matrix}(Iota,Iota,\mathbb{C}),(\mathrm{ExactPreparationContract}(R,K))\Rightarrow (\exists c:\mathbb{R},(0<c)\wedge \\ (\forall X:\mathrm{Matrix}(Iota,Iota,\mathbb{C}),\mathrm{ofKraus}(K,K,X)=c\cdot \mathrm{sqrt}(R)\cdot X\cdot \mathrm{sqrt}(R))))\wedge \\ (\forall c:\mathbb{R},(0<c)\Rightarrow (\mathrm{let}Kc:(\mathrm{Fin}(1))\to \mathrm{Matrix}(Iota,Iota,\mathbb{C}):=fu{n}_{\mapsto }\mathrm{sqrt}(c)\cdot \mathrm{sqrt}(R);(\forall rho:\mathrm{Matrix}(Iota,Iota,\mathbb{C}),((\mathrm{PosSemidef}(rho))\wedge \\ (\mathrm{Tr}(rho)=1))\Rightarrow ((0<\mathrm{Re}(\mathrm{Tr}(\mathrm{ofKraus}(Kc,Kc,rho))))\wedge \\ (\mathrm{ofKraus}(Kc,Kc,rho)=\mathrm{Tr}(\mathrm{ofKraus}(Kc,Kc,rho))/\mathrm{Tr}(R\cdot rho)\cdot \mathrm{sqrt}(R)\cdot rho\cdot \mathrm{sqrt}(R))))\wedge \\ (\mathrm{TraceNonincreasing}(Kc)⟺\mathrm{PosSemidef}(I-c\cdot R))))\wedge \\ (\forall m:\mathbb{N},\forall K:(\mathrm{Fin}(m))\to \mathrm{Matrix}(Iota,Iota,\mathbb{C}),\forall c:\mathbb{R},(0<c)\Rightarrow ((\forall X:\mathrm{Matrix}(Iota,Iota,\mathbb{C}),\mathrm{ofKraus}(K,K,X)=c\cdot \mathrm{sqrt}(R)\cdot X\cdot \mathrm{sqrt}(R))\Rightarrow (\mathrm{TraceNonincreasing}(K)⟺\mathrm{PosSemidef}(I-c\cdot R))))\wedge \\ (\forall m:\mathbb{N},\forall K:(\mathrm{Fin}(m))\to \mathrm{Matrix}(Iota,Iota,\mathbb{C}),(\mathrm{ExactPreparationContract}(R,K))\Rightarrow ((\mathrm{TraceNonincreasing}(K))\Rightarrow (\exists rho:\mathrm{Matrix}(Iota,Iota,\mathbb{C}),((\mathrm{PosSemidef}(rho))\wedge \\ (\mathrm{Tr}(rho)=1))\wedge \\ (\mathrm{Re}(\mathrm{Tr}(\mathrm{ofKraus}(K,K,rho)))\le \mathrm{leastEigenvalue}(R)/\mathrm{greatestEigenvalue}(R)))))\wedge \\ (\mathrm{let}Kopt:(\mathrm{Fin}(1))\to \mathrm{Matrix}(Iota,Iota,\mathbb{C}):=fu{n}_{\mapsto }1/\sqrt{\mathrm{greatestEigenvalue}(R)}\cdot \mathrm{sqrt}(R);\mathrm{let}Kfail:\mathrm{Matrix}(Iota,Iota,\mathbb{C}):=\mathrm{sqrt}(1-1/\mathrm{greatestEigenvalue}(R)\cdot R);(\mathrm{ExactPreparationContract}(R,Kopt))\wedge \\ (\mathrm{TraceNonincreasing}(Kopt))\wedge \\ (\mathrm{conjTranspose}(Kopt(0))\cdot Kopt(0)+\mathrm{conjTranspose}(Kfail)\cdot Kfail=I)\wedge \\ (\forall rho:\mathrm{Matrix}(Iota,Iota,\mathbb{C}),((\mathrm{PosSemidef}(rho))\wedge \\ (\mathrm{Tr}(rho)=1))\Rightarrow (\mathrm{leastEigenvalue}(R)/\mathrm{greatestEigenvalue}(R)\le \mathrm{Re}(\mathrm{Tr}(\mathrm{ofKraus}(Kopt,Kopt,rho))))))\wedge \\ ((\exists m:\mathbb{N},\exists K:(\mathrm{Fin}(m))\to \mathrm{Matrix}(Iota,Iota,\mathbb{C}),(\mathrm{ExactPreparationContract}(R,K))\wedge \\ (\mathrm{TraceNonincreasing}(K))\wedge \\ (\forall rho:\mathrm{Matrix}(Iota,Iota,\mathbb{C}),((\mathrm{PosSemidef}(rho))\wedge \\ (\mathrm{Tr}(rho)=1))\Rightarrow (\mathrm{Tr}(\mathrm{ofKraus}(K,K,rho))=1)))⟺\exists lambda:\mathbb{R},(0<lambda)\wedge \\ (R=lambda\cdot I)). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Every exact universal preparation family is a positive scalar multiple of the square-root sandwich channel. Its total effect is the same scalar multiple of the prescribed effect, so trace nonincrease bounds the scalar by the reciprocal largest eigenvalue. A largest-eigenvalue input gives the upper bound, while the reciprocal-square-root filter attains the least-to-largest eigenvalue ratio. Deterministic preparation is possible exactly when the effect is a positive scalar identity.

References

• Truth anchor: D5/S3/Quantum/Measurement/ExactConditionalPreparationCost.ExactPreparationContract
• Truth anchor: D5/S3/Quantum/Measurement/ExactConditionalPreparationCost.TraceNonincreasing
• Truth anchor: D5/S3/Quantum/Measurement/ExactConditionalPreparationCost.exact_conditional_preparation_cost
• Truth anchor: D5/S3/Quantum/Measurement/ExactConditionalPreparationCost.greatestEigenvalue
• Truth anchor: D5/S3/Quantum/Measurement/ExactConditionalPreparationCost.leastEigenvalue
• Dependency: D5/S3/Quantum/Foundation/FiniteKrausChannel
• Dependency: D5/S3/Quantum/Measurement/FiniteKrausInstrumentBornMarginal
• Dependency: D5/S3/Quantum/PureState/PureStateHandshake