TracePreservingEigenvalueBound

Abstract

TracePreservingEigenvalueBound for the spectral bound of conditionally two-positive maps.

Definition 1.1 (Source Theorem 1 Bound).

$$\forall (d:\mathbb{N}),\forall (\varphi :(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}{\to }_{l[\mathbb{C}]}\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),SourceTheorem1Bound\varphi \iff ((\mathrm{LinearMap}.\mathrm{trace}\mathbb{C}(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})\varphi )).\mathrm{re}\le (d:\mathbb{R})\ast \mathrm{minReSpectrum}\varphi +((d:\mathbb{R}{)}^2-d)$$

Formalization. D5/S3/Quantum/QuantumChannels/TracePreservingEigenvalueBound.SourceTheorem1Bound (✓ std3).

Citation. F. vom Ende, D. Chruściński, G. Kimura, P. Muratore-Ginanneschi (2025). Universal Bound on the Eigenvalues of 2-Positive Trace-Preserving Maps. DOI: 10.1016/j.laa.2025.10.022. URL: https://arxiv.org/abs/2506.02145v1.

Commentary.

The displayed statement gives the hypotheses and conclusion for SourceTheorem1Bound. Matrices are complex matrices of the displayed finite dimension; LinearMap.trace denotes the endomorphism trace. All sums over Fin d run over its full finite universe.

Definition 1.2 (Source Theorem 1 Goal).

$$SourceTheorem1Goal\iff \forall (d:\mathbb{N}),0<d\to \forall \varphi :(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}{\to }_{l[\mathbb{C}]}\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}),(\mathrm{KPositive}2d\varphi )\to (\forall X,\mathrm{Matrix}.\mathrm{trace}(\varphi X)=\mathrm{Matrix}.\mathrm{trace}X)\to SourceTheorem1Bound\varphi$$

Formalization. D5/S3/Quantum/QuantumChannels/TracePreservingEigenvalueBound.SourceTheorem1Goal (✓ std3).

Citation. F. vom Ende, D. Chruściński, G. Kimura, P. Muratore-Ginanneschi (2025). Universal Bound on the Eigenvalues of 2-Positive Trace-Preserving Maps. DOI: 10.1016/j.laa.2025.10.022. URL: https://arxiv.org/abs/2506.02145v1.

Commentary.

Theorem 1, page 4, arXiv:2506.02145v1: “Let Φ ∈ L(ℂ^{d×d}) be a 2-positive and trace-preserving linear map. Then” tr(Φ) ≤ d min ℜ(σ(Φ)) + (d² − d). Trace preservation is equality of Matrix.trace before and after Φ for every matrix.

Definition 1.3 (congrEquiv).

$$\forall (d:\mathbb{N})(RS:\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})(\mathrm{hRS}:R\ast S=1)(\mathrm{hSR}:S\ast R=1),(\mathrm{congrEquiv}RS\mathrm{hRS}\mathrm{hSR}).\mathrm{toLinearMap}=\mathrm{LinearMap}.\mathrm{mulLeftRight}\mathbb{C}(R,R.\mathrm{conjTranspose})\wedge (\mathrm{congrEquiv}RS\mathrm{hRS}\mathrm{hSR}).\mathrm{symm}.\mathrm{toLinearMap}=\mathrm{LinearMap}.\mathrm{mulLeftRight}\mathbb{C}(S,S.\mathrm{conjTranspose})$$

Formalization. D5/S3/Quantum/QuantumChannels/TracePreservingEigenvalueBound.congrEquiv (✓ std3).

Source. Repository-derived.

Acknowledgement. F. vom Ende, D. Chruściński, G. Kimura, P. Muratore-Ginanneschi (2025). Universal Bound on the Eigenvalues of 2-Positive Trace-Preserving Maps. DOI: 10.1016/j.laa.2025.10.022. URL: https://arxiv.org/abs/2506.02145v1.

Commentary.

The displayed statement gives the hypotheses and conclusion for congrEquiv. Matrices are complex matrices of the displayed finite dimension; LinearMap.trace denotes the endomorphism trace. All sums over Fin d run over its full finite universe.

Theorem 1.4 (hsAdjoint trace).

$$\forall (d:\mathbb{N}),[\mathrm{hsInner}],\forall (\mathrm{Phi}:(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}{\to }_{l[\mathbb{C}]}\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),\mathrm{LinearMap}.\mathrm{trace}\mathbb{C}((\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}))(\mathrm{LinearMap}.\mathrm{adjoint}\mathrm{Phi})=\mathrm{star}(\mathrm{LinearMap}.\mathrm{trace}\mathbb{C}((\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}))\mathrm{Phi})$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TracePreservingEigenvalueBound.hsAdjoint_trace (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. F. vom Ende, D. Chruściński, G. Kimura, P. Muratore-Ginanneschi (2025). Universal Bound on the Eigenvalues of 2-Positive Trace-Preserving Maps. DOI: 10.1016/j.laa.2025.10.022. URL: https://arxiv.org/abs/2506.02145v1.

Commentary.

The displayed statement gives the hypotheses and conclusion for hsAdjoint_trace. Matrices are complex matrices of the displayed finite dimension; LinearMap.trace denotes the endomorphism trace. All sums over Fin d run over its full finite universe.

Theorem 1.5 (extrema hsAdjoint).

$$\forall (d:\mathbb{N}),[\mathrm{hsInner}],\forall (\mathrm{Phi}:(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}{\to }_{l[\mathbb{C}]}\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),\mathrm{minReSpectrum}(\mathrm{LinearMap}.\mathrm{adjoint}\mathrm{Phi})=\mathrm{minReSpectrum}\mathrm{Phi}\wedge \mathrm{maxReSpectrum}(\mathrm{LinearMap}.\mathrm{adjoint}\mathrm{Phi})=\mathrm{maxReSpectrum}\mathrm{Phi}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TracePreservingEigenvalueBound.extrema_hsAdjoint (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. F. vom Ende, D. Chruściński, G. Kimura, P. Muratore-Ginanneschi (2025). Universal Bound on the Eigenvalues of 2-Positive Trace-Preserving Maps. DOI: 10.1016/j.laa.2025.10.022. URL: https://arxiv.org/abs/2506.02145v1.

Commentary.

The displayed statement gives the hypotheses and conclusion for extrema_hsAdjoint. Matrices are complex matrices of the displayed finite dimension; LinearMap.trace denotes the endomorphism trace. All sums over Fin d run over its full finite universe.

Theorem 1.6 (extrema conj).

$$\forall (d:\mathbb{N}),\forall (e:(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}){\equiv }_{l[\mathbb{C}]}(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),\forall (\mathrm{Phi}:(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}{\to }_{l[\mathbb{C}]}\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),\mathrm{minReSpectrum}(e.\mathrm{conj}\mathrm{Phi})=\mathrm{minReSpectrum}\mathrm{Phi}\wedge \mathrm{maxReSpectrum}(e.\mathrm{conj}\mathrm{Phi})=\mathrm{maxReSpectrum}\mathrm{Phi}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TracePreservingEigenvalueBound.extrema_conj (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. F. vom Ende, D. Chruściński, G. Kimura, P. Muratore-Ginanneschi (2025). Universal Bound on the Eigenvalues of 2-Positive Trace-Preserving Maps. DOI: 10.1016/j.laa.2025.10.022. URL: https://arxiv.org/abs/2506.02145v1.

Commentary.

The displayed statement gives the hypotheses and conclusion for extrema_conj. Matrices are complex matrices of the displayed finite dimension; LinearMap.trace denotes the endomorphism trace. All sums over Fin d run over its full finite universe.

Theorem 1.7 (faithful fourth roots).

$$\forall (d:\mathbb{N}),\forall (\mathrm{rho}:(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),(\mathrm{rho}.\mathrm{PosDef})\to \exists RS:(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}),R.\mathrm{IsHermitian}\wedge S.\mathrm{IsHermitian}\wedge R\ast S=1\wedge S\ast R=1\wedge (S\ast S)\ast (S\ast S)=\mathrm{rho}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TracePreservingEigenvalueBound.faithful_fourth_roots (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. F. vom Ende, D. Chruściński, G. Kimura, P. Muratore-Ginanneschi (2025). Universal Bound on the Eigenvalues of 2-Positive Trace-Preserving Maps. DOI: 10.1016/j.laa.2025.10.022. URL: https://arxiv.org/abs/2506.02145v1.

Commentary.

The displayed statement gives the hypotheses and conclusion for faithful_fourth_roots. Matrices are complex matrices of the displayed finite dimension; LinearMap.trace denotes the endomorphism trace. All sums over Fin d run over its full finite universe.

Theorem 1.8 (theorem1 general).

$$SourceTheorem1Goal$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TracePreservingEigenvalueBound.theorem1_general (✓ std3). ∎

Citation. F. vom Ende, D. Chruściński, G. Kimura, P. Muratore-Ginanneschi (2025). Universal Bound on the Eigenvalues of 2-Positive Trace-Preserving Maps. DOI: 10.1016/j.laa.2025.10.022. URL: https://arxiv.org/abs/2506.02145v1.

Commentary.

Theorem 1, page 4, arXiv:2506.02145v1: “Let Φ ∈ L(ℂ^{d×d}) be a 2-positive and trace-preserving linear map. Then” tr(Φ) ≤ d min ℜ(σ(Φ)) + (d² − d). SourceTheorem1Goal states this for every positive dimension. The weighted Hilbert–Schmidt symmetric part supplies a real eigenvalue no larger than the real part of any original eigenvalue. Diagonalization then gives the transition estimate; depolarizing approximation removes faithfulness of the invariant state.

Definition 1.9 (depolarized).

$$\forall (d:\mathbb{N}),\forall (\mathrm{Phi}:((\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}){\to }_{l[\mathbb{C}]}(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}))),\forall (\epsilon :\mathbb{R}),\mathrm{depolarized}\mathrm{Phi}\epsilon =((((1-\epsilon ):\mathbb{R}):\mathbb{C}))\cdot (\mathrm{Phi})+(((\frac{\epsilon }{d}:\mathbb{R}):\mathbb{C}))\cdot (((\mathrm{Matrix}.\mathrm{traceLinearMap}(\mathrm{Fin}d)\mathbb{CC}).\mathrm{smulRight}(1:(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}))))$$

Formalization. D5/S3/Quantum/QuantumChannels/TracePreservingEigenvalueBound.depolarized (✓ std3).

Source. Repository-derived.

Acknowledgement. F. vom Ende, D. Chruściński, G. Kimura, P. Muratore-Ginanneschi (2025). Universal Bound on the Eigenvalues of 2-Positive Trace-Preserving Maps. DOI: 10.1016/j.laa.2025.10.022. URL: https://arxiv.org/abs/2506.02145v1.

Commentary.

This is the depolarized channel (1−ε)Φ + ε Tr(·)I/d; the real coefficients are cast to ℂ, with Matrix.traceLinearMap and LinearMap.smulRight supplying the trace-times-identity term.

References

• Truth anchor: D5/S3/Quantum/QuantumChannels/TracePreservingEigenvalueBound.SourceTheorem1Bound
• Truth anchor: D5/S3/Quantum/QuantumChannels/TracePreservingEigenvalueBound.SourceTheorem1Goal
• Truth anchor: D5/S3/Quantum/QuantumChannels/TracePreservingEigenvalueBound.congrEquiv
• Truth anchor: D5/S3/Quantum/QuantumChannels/TracePreservingEigenvalueBound.depolarized
• Truth anchor: D5/S3/Quantum/QuantumChannels/TracePreservingEigenvalueBound.extrema_conj
• Truth anchor: D5/S3/Quantum/QuantumChannels/TracePreservingEigenvalueBound.extrema_hsAdjoint
• Truth anchor: D5/S3/Quantum/QuantumChannels/TracePreservingEigenvalueBound.faithful_fourth_roots
• Truth anchor: D5/S3/Quantum/QuantumChannels/TracePreservingEigenvalueBound.hsAdjoint_trace
• Truth anchor: D5/S3/Quantum/QuantumChannels/TracePreservingEigenvalueBound.theorem1_general
• Dependency: D5/S3/Quantum/ChannelFixedState
• Dependency: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace