TwoPositiveTransitionTrace

Abstract

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

Lemma 1.1 (Trace in the matrix-unit basis).

$$\forall (d:\mathbb{N}),\forall (\varphi :\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right){\to }_{l[\mathbb{C}]}\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)),\mathrm{LinearMap}.\mathrm{trace}\left(\mathbb{C},\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\varphi \right)=\sum i:\mathrm{Fin}\left(d\right),\sum j:\mathrm{Fin}\left(d\right),\varphi \left(\mathrm{Matrix}.\mathrm{single}\left(i,j,1\right),i,j\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.trace_standard (✓ 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 trace of a complex-linear map on finite square matrices is the sum of its diagonal coefficients in the matrix-unit basis.

Lemma 1.2 (Trace against a rank-one matrix).

$$\forall n\in \mathrm{Type},[\mathrm{Fintype}\left(n\right)][\mathrm{DecidableEq}\left(n\right)]\forall X\in \mathrm{Matrix}\left(n,n,\mathbb{C}\right),\forall v\in n\to \mathbb{C},\mathrm{Matrix}.\mathrm{trace}\left(X\cdot \mathrm{Matrix}.\mathrm{vecMulVec}\left(v,\mathrm{star}\left(v\right)\right)\right)=\mathrm{dotProduct}\left(\mathrm{star}\left(v\right),\mathrm{Matrix}.\mathrm{mulVec}\left(X,v\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.trace_rank_one (✓ 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.

For any finite complex matrix X and vector v, the trace of X times the rank-one matrix of v equals the scalar product of star v with X applied to v.

Definition 1.3 (minReSpectrum).

$$\forall (d:\mathbb{N})(L:(\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}L=\mathrm{sInf}(\mathrm{Set}.\mathrm{image}\mathrm{Complex}.\mathrm{re}(\{z:\mathbb{C}|z\in L.\mathrm{charpoly}.\mathrm{roots}\}))$$

Formalization. D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.minReSpectrum (✓ 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 minReSpectrum. 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.4 (maxReSpectrum).

$$\forall (d:\mathbb{N})(L:(\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{maxReSpectrum}L=\mathrm{sSup}(\mathrm{Set}.\mathrm{image}\mathrm{Complex}.\mathrm{re}(\{z:\mathbb{C}|z\in L.\mathrm{charpoly}.\mathrm{roots}\}))$$

Formalization. D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.maxReSpectrum (✓ 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 maxReSpectrum. 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.5 (spectralBound).

$$\forall (d:\mathbb{N}),\forall (L:(\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{spectralBound}L\iff ((\mathrm{LinearMap}.\mathrm{trace}\mathbb{C}(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})L)).\mathrm{re}\le (d:\mathbb{R})\ast \mathrm{minReSpectrum}L+((d:\mathbb{R}{)}^2-d)\ast \mathrm{maxReSpectrum}L$$

Formalization. D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.spectralBound (✓ 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 spectralBound. 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 (pair extraction).

$$\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})),((\mathrm{KPositive}2d\varphi ))\to \forall (jk:\mathrm{Fin}d),(\varphi (\mathrm{Matrix}.\mathrm{single}kj1)kj).\mathrm{re}+(\varphi (\mathrm{Matrix}.\mathrm{single}jk1)jk).\mathrm{re}\le (\varphi (\mathrm{Matrix}.\mathrm{single}kk1)kk).\mathrm{re}+(\varphi (\mathrm{Matrix}.\mathrm{single}jj1)jj).\mathrm{re}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.pair_extraction (✓ 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 pair estimate in the proof of Lemma 1, page 7, arXiv:2506.02145v1. Testing the amplified map on the entangled rank-one matrix formed from two matrix units and using the opposite-sign vector bounds the two crossed diagonal coefficients by the two uncrossed coefficients.

Theorem 1.7 (transition trace 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})),((\mathrm{KPositive}2d\varphi ))\to (\mathrm{LinearMap}.\mathrm{trace}\mathbb{C}((\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}))\varphi ).\mathrm{re}\le (d:\mathbb{R})\ast \sum i:\mathrm{Fin}d,(\varphi (\mathrm{Matrix}.\mathrm{single}ii1)ii).\mathrm{re}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.transition_trace_bound (✓ 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.

Lemma 1, page 6, arXiv:2506.02145v1, equation (8), specialized to the standard orthonormal basis. Summing the pair estimates over every ordered pair yields the dimension-wide superoperator trace estimate. LinearMap.trace is the trace on the matrix space, rather than Matrix.trace of an output matrix.

Theorem 1.8 (twoPositive star preserving).

$$\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})),((\mathrm{KPositive}2d\varphi ))\to \forall (Y:(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),\varphi Y.\mathrm{conjTranspose}=(\varphi Y).\mathrm{conjTranspose}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.twoPositive_star_preserving (✓ 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 twoPositive_star_preserving. 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.9 (twoPositive add).

$$\forall (d:\mathbb{N}),\forall (\varphi \psi :(\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 ((\mathrm{KPositive}2d\psi ))\to (\mathrm{KPositive}2d(\varphi +\psi ))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.twoPositive_add (✓ 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 twoPositive_add. 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.10 (twoPositive smul).

$$\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})),((\mathrm{KPositive}2d\varphi ))\to \forall (c:\mathbb{R}),(0\le c)\to (\mathrm{KPositive}2d((c:\mathbb{C})\cdot \varphi ))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.twoPositive_smul (✓ 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 twoPositive_smul. 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.11 (traceIdentity twoPositive).

$$\forall (d:\mathbb{N}),(\mathrm{KPositive}2d(((\mathrm{Matrix}.\mathrm{traceLinearMap}(\mathrm{Fin}d)\mathbb{CC}).\mathrm{smulRight}(1:\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.traceIdentity_twoPositive (✓ 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 traceIdentity_twoPositive. 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.12 (regularization twoPositive).

$$\forall (d:\mathbb{N}),\forall (T:(\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}2dT))\to \forall (\epsilon :\mathbb{R}),(0\le \epsilon )\to (\mathrm{KPositive}2d(T+(\epsilon :\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}))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.regularization_twoPositive (✓ 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 regularization_twoPositive. 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.13 (twoPositive positive).

$$\forall (d:\mathbb{N}),\forall (T:(\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}2dT))\to \forall (X:(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),(X.\mathrm{PosSemidef})\to (TX).\mathrm{PosSemidef}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.twoPositive_positive (✓ 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 twoPositive_positive. 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.14 (regularization strictly improving).

$$\forall (d:\mathbb{N}),\forall (T:(\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}2dT))\to \forall (\epsilon :\mathbb{R}),(0<\epsilon )\to \forall (X:(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),(X.\mathrm{PosSemidef})\to (X\ne 0)\to (((T+(\epsilon :\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}))):(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}{\to }_{l[\mathbb{C}]}\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}))X).\mathrm{PosDef}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.regularization_strictly_improving (✓ 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 regularization_strictly_improving. 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.15 (positive diag of two).

$$\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})),((\mathrm{KPositive}2d\varphi ))\to \forall (ij:\mathrm{Fin}d),0\le (\varphi (\mathrm{Matrix}.\mathrm{single}jj1)ii).\mathrm{re}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.positive_diag_of_two (✓ 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 positive_diag_of_two. 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.16 (transition).

$$\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})),\mathrm{transition}\varphi =\lambda ij\mapsto (\varphi (\mathrm{Matrix}.\mathrm{single}jj1)ii)$$

Formalization. D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.transition (✓ 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.

Page 6, arXiv:2506.02145v1: “given Φ ∈ L(Cd×d) and any orthonormal basis G := {gj}dj=1 of Cd define TG(Φ) ∈ Cd×d (or TG, for short) via (TG)jk := ⟨gj|Φ(|gk⟩⟨gk|)|gj⟩.” In the standard basis the entry is Phi (Matrix.single j j 1) i i, with its full complex value. Fin d indexes all d basis vectors.

Theorem 1.17 (transition colStochastic).

$$\forall (d:\mathbb{N}),[\mathrm{NeZero}d],\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})),(\forall ij:\mathrm{Fin}d,0\le (\varphi (\mathrm{Matrix}.\mathrm{single}jj1)ii).\mathrm{re})\to ((\forall X,\mathrm{Matrix}.\mathrm{trace}(\varphi X)=\mathrm{Matrix}.\mathrm{trace}X))\to (\mathrm{transition}\varphi ).\mathrm{map}\mathrm{Complex}.\mathrm{re}\in \mathrm{Matrix}.\mathrm{colStochastic}\mathbb{R}(\mathrm{Fin}d)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.transition_colStochastic (✓ 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 transition_colStochastic. 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.18 (hsInner).

$$\forall (d:\mathbb{N}),\mathrm{hsInner}.\mathrm{toNormedSpace}=\mathrm{Matrix}.\mathrm{frobeniusNormedSpace}\wedge \forall (XY:\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}),\mathrm{hsInner}.\mathrm{inner}XY=(X.\mathrm{conjTranspose}\ast Y).\mathrm{trace}$$

Formalization. D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.hsInner (✓ 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 Hilbert–Schmidt structure uses the Frobenius norm already supplied by Mathlib. Its inner product is exactly the trace of conjTranspose X times Y; the normed-space field is Matrix.frobeniusNormedSpace. The equality specifies the data fields; the remaining structure fields certify the inner-product laws.

Definition 1.19 (weightedAdjoint).

$$\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})),\forall (WV:(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),\mathrm{weightedAdjoint}\mathrm{Phi}WV=((\mathrm{LinearMap}.\mathrm{mulLeftRight}\mathbb{C}(W,W.\mathrm{conjTranspose}))).\mathrm{comp}((\mathrm{LinearMap}.\mathrm{adjoint}\mathrm{Phi}).\mathrm{comp}((\mathrm{LinearMap}.\mathrm{mulLeftRight}\mathbb{C}(V,V.\mathrm{conjTranspose}))))$$

Formalization. D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.weightedAdjoint (✓ 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 weightedAdjoint. 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.20 (hsAdjoint inner left).

$$\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})),\forall (XY:(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),\mathrm{inner}\mathbb{C}(\mathrm{LinearMap}.\mathrm{adjoint}\mathrm{Phi}Y)X=\mathrm{inner}\mathbb{C}Y(\mathrm{Phi}X)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.hsAdjoint_inner_left (✓ 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_inner_left. 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.21 (hsAdjoint entry).

$$\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})),\forall (Y:(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),\forall (ab:\mathrm{Fin}d),\mathrm{LinearMap}.\mathrm{adjoint}\mathrm{Phi}Yab=\sum i:\mathrm{Fin}d,\sum j:\mathrm{Fin}d,\mathrm{star}(\mathrm{Phi}(\mathrm{Matrix}.\mathrm{single}ab1)ij)\ast Yij$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.hsAdjoint_entry (✓ 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_entry. 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.22 (unital iff adjoint tracePreserving).

$$\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{Phi}1=1\iff (\forall X,\mathrm{Matrix}.\mathrm{trace}((\mathrm{LinearMap}.\mathrm{adjoint}\mathrm{Phi})X)=\mathrm{Matrix}.\mathrm{trace}X)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.unital_iff_adjoint_tracePreserving (✓ 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 unital_iff_adjoint_tracePreserving. 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.23 (adjoint twoPositive).

$$\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{KPositive}2d\mathrm{Phi}))\to (\mathrm{KPositive}2d(\mathrm{LinearMap}.\mathrm{adjoint}\mathrm{Phi}))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.adjoint_twoPositive (✓ 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 adjoint_twoPositive. 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.24 (congrMap twoPositive).

$$\forall (d:\mathbb{N}),\forall (A:(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})),(\mathrm{KPositive}2d((\mathrm{LinearMap}.\mathrm{mulLeftRight}\mathbb{C}(A,A.\mathrm{conjTranspose}))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.congrMap_twoPositive (✓ 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 congrMap_twoPositive. 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.25 (twoPositive comp).

$$\forall (d:\mathbb{N}),\forall (TS:(\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}2dT))\to ((\mathrm{KPositive}2dS))\to (\mathrm{KPositive}2d(T.\mathrm{comp}S))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.twoPositive_comp (✓ 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 twoPositive_comp. 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.26 (superoperator trace real twoPositive).

$$\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})),((\mathrm{KPositive}2d\varphi ))\to (\mathrm{LinearMap}.\mathrm{trace}\mathbb{C}((\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}))\varphi ).\mathrm{im}=0$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.superoperator_trace_real_twoPositive (✓ 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 superoperator_trace_real_twoPositive. 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.27 (faithful fixed eigenvalue norm le one).

$$\forall (A:\mathrm{Type}\ast ),[\mathrm{CStarAlgebra}A],[\mathrm{PartialOrder}A],[\mathrm{StarOrderedRing}A],[\mathrm{NonnegSpectrumClass}\mathbb{R}A],[\mathrm{Nontrivial}A],[\mathrm{NormOneClass}A],\forall (U:(A{\to }_{l[\mathbb{C}]}A)),(\forall X,0\le X\to 0\le UX)\to \forall (\rho :A),(\mathrm{IsStrictlyPositive}\rho )\to (U\rho =\rho )\to \forall (z:\mathbb{C}),(\mathrm{Module}.\mathrm{End}.\mathrm{HasEigenvalue}Uz)\to \Vert z\Vert \le 1$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.faithful_fixed_eigenvalue_norm_le_one (✓ 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.

A strictly positive invariant element bounds the order unit from below. Positivity of every power then bounds its action uniformly on every eigenvector. An eigenvalue of modulus greater than one would contradict this bound through geometric growth.

Theorem 1.28 (root mem iff).

$$\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 (z:\mathbb{C}),z\in (\mathrm{Phi}.\mathrm{charpoly}.\mathrm{roots})\iff \mathrm{Module}.\mathrm{End}.\mathrm{HasEigenvalue}\mathrm{Phi}z$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.root_mem_iff (✓ 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 root_mem_iff. 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.29 (roots finite).

$$\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})),\{z:\mathbb{C}|z\in (\mathrm{Phi}.\mathrm{charpoly}.\mathrm{roots})\}.\mathrm{Finite}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.roots_finite (✓ 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 roots_finite. 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.30 (roots nonempty).

$$\forall (d:\mathbb{N}),[\mathrm{NeZero}d],\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})),\{z:\mathbb{C}|z\in (\mathrm{Phi}.\mathrm{charpoly}.\mathrm{roots})\}.\mathrm{Nonempty}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.roots_nonempty (✓ 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 roots_nonempty. 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.31 (extrema tendsto).

$$\forall (d:\mathbb{N}),[\mathrm{NeZero}d],\forall (\alpha :\mathrm{Type}\ast ),\forall (l:\mathrm{Filter}\alpha ),\forall (A:\alpha \to (\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 (B:(\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{Tendsto}Al(\mathrm{nhds}B))\to \mathrm{Tendsto}(\lambda x\mapsto \mathrm{minReSpectrum}(Ax).\mathrm{toLinearMap})l(\mathrm{nhds}(\mathrm{minReSpectrum}B.\mathrm{toLinearMap}))\wedge \mathrm{Tendsto}(\lambda x\mapsto \mathrm{maxReSpectrum}(Ax).\mathrm{toLinearMap})l(\mathrm{nhds}(\mathrm{maxReSpectrum}B.\mathrm{toLinearMap}))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.extrema_tendsto (✓ 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_tendsto. 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.32 (superTrace continuous).

$$\forall (d:\mathbb{N}),\mathrm{Continuous}(\lambda L:(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C}{\to }_{L[\mathbb{C}]}\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})\mapsto (\mathrm{LinearMap}.\mathrm{trace}\mathbb{C}(\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}d)\mathbb{C})L.\mathrm{toLinearMap}))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.superTrace_continuous (✓ 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 superTrace_continuous. 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.

References

• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.adjoint_twoPositive
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.congrMap_twoPositive
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.extrema_tendsto
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.faithful_fixed_eigenvalue_norm_le_one
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.hsAdjoint_entry
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.hsAdjoint_inner_left
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.hsInner
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.maxReSpectrum
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.minReSpectrum
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.pair_extraction
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.positive_diag_of_two
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.regularization_strictly_improving
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.regularization_twoPositive
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.root_mem_iff
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.roots_finite
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.roots_nonempty
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.spectralBound
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.superTrace_continuous
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.superoperator_trace_real_twoPositive
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.traceIdentity_twoPositive
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.trace_rank_one
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.trace_standard
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.transition
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.transition_colStochastic
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.transition_trace_bound
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.twoPositive_add
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.twoPositive_comp
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.twoPositive_positive
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.twoPositive_smul
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.twoPositive_star_preserving
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.unital_iff_adjoint_tracePreserving
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwoPositiveTransitionTrace.weightedAdjoint
• Dependency: D5/S3/Quantum/QuantumChannels/TomiyamaDiagonalKPositivity