Elementary channel divisibility

Abstract

Exact Kraus-space criterion for elementary right division of finite quantum channels.

The index type I is finite. Matrices act on the complex coordinate space I → ℂ. The inner product is conjugate linear in its first argument, and tr denotes Matrix.trace. CP is the existing complete-positivity predicate, quantifying every finite amplification; CPTP also preserves the trace of every matrix. No assertion about a physical gate set, a local operations protocol, a success probability or a preparation cost follows from these statements.

Theorem 1.1 (Matrix factorization from kernel inclusion).

$$\forall (I:\mathrm{Type}),\forall [(\mathrm{Fintype}(I))][(\mathrm{DecidableEq}(I))],\forall (R:(\mathrm{Matrix}(I,I,\mathbb{C}))),\forall (S:(\mathrm{Matrix}(I,I,\mathbb{C}))),((\forall (v:(I\to \mathbb{C})),(((\mathrm{mulVec}(R,v))=0)\to ((\mathrm{mulVec}(S,v))=0)))\to (\exists (C:(\mathrm{Matrix}(I,I,\mathbb{C}))),S=(CR)))$$

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

Source. Repository-derived.

Acknowledgement. Frederik vom Ende (2024). A Sufficient Criterion for Divisibility of Quantum Channels. DOI: 10.1063/5.0231812. URL: https://arxiv.org/html/2407.17103v3.

Commentary.

If every vector annihilated by R is also annihilated by S, then S factors as CR. The linear map induced by S on the quotient by ker R descends to the range of R and extends to the whole finite coordinate space.

Theorem 1.2 (Kernel inclusion from positive domination).

$$\forall (I:\mathrm{Type}),\forall [(\mathrm{Fintype}(I))][(\mathrm{DecidableEq}(I))],\forall (A:(\mathrm{Matrix}(I,I,\mathbb{C}))),\forall (B:(\mathrm{Matrix}(I,I,\mathbb{C}))),\forall (t:\mathbb{R}),(((((\mathrm{PosSemidef}(B)))\wedge (0<t)\wedge ((\mathrm{PosSemidef}((A-((t)\cdot (B))))))))\to (\forall (v:(I\to \mathbb{C})),(((\mathrm{mulVec}(A,v))=0)\to ((\mathrm{mulVec}(B,v))=0))))$$

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

Source. Repository-derived.

Acknowledgement. Frederik vom Ende (2024). A Sufficient Criterion for Divisibility of Quantum Channels. DOI: 10.1063/5.0231812. URL: https://arxiv.org/html/2407.17103v3.

Commentary.

If B and A − tB are positive semidefinite and t > 0, every vector annihilated by A is annihilated by B. On such a vector the two positivity inequalities force the quadratic form of B to vanish, and positive semidefiniteness then forces B to annihilate the vector.

Definition 1.3 (Ordered orthogonal unit pair).

$$\forall (I:\mathrm{Type}),\forall [(\mathrm{Fintype}(I))][(\mathrm{DecidableEq}(I))],\forall (x:(I\to \mathbb{C})),\forall (y:(I\to \mathbb{C})),(((\mathrm{OrthogonalUnitPair}(x,y)))\iff (((⟨x,x⟩=1)\wedge (⟨y,y⟩=1)\wedge (⟨x,y⟩=0))))$$

Formalization. D5/S3/Quantum/QuantumChannels/ElementaryChannelDivisibility.OrthogonalUnitPair (✓ std3).

Citation. Frederik vom Ende (2024). A Sufficient Criterion for Divisibility of Quantum Channels. DOI: 10.1063/5.0231812. URL: https://arxiv.org/html/2407.17103v3.

Commentary.

The two vectors are separately normalized and orthogonal in the displayed order.

Theorem 1.4 (Distinct coordinate vectors form an orthogonal unit pair).

$$\forall (I:\mathrm{Type}),\forall [(\mathrm{Fintype}(I))][(\mathrm{DecidableEq}(I))],\forall (r:I),\forall (s:I),((r\ne s)\to ((\mathrm{OrthogonalUnitPair}((\mathrm{Pi}.\mathrm{single}(r,1)),(\mathrm{Pi}.\mathrm{single}(s,1))))))$$

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

Source. Repository-derived.

Acknowledgement. Frederik vom Ende (2024). A Sufficient Criterion for Divisibility of Quantum Channels. DOI: 10.1063/5.0231812. URL: https://arxiv.org/html/2407.17103v3.

Commentary.

Two distinct coordinate vectors have unit norm and zero ordered inner product.

Definition 1.5 (Rank one operator).

$$\forall (I:\mathrm{Type}),\forall [(\mathrm{Fintype}(I))][(\mathrm{DecidableEq}(I))],\forall (u:(I\to \mathbb{C})),\forall (v:(I\to \mathbb{C})),(\mathrm{ketbra}(u,v))=(\mathrm{vecMulVec}(u,(\mathrm{star}(v))))$$

Formalization. D5/S3/Quantum/QuantumChannels/ElementaryChannelDivisibility.ketbra (✓ std3).

Citation. Frederik vom Ende (2024). A Sufficient Criterion for Divisibility of Quantum Channels. DOI: 10.1063/5.0231812. URL: https://arxiv.org/html/2407.17103v3.

Commentary.

The operator ketbra(u,v) sends z to u⟨v,z⟩.

Theorem 1.6 (Adjoint of a rank one operator).

$$\forall (n:\mathrm{Type}),\forall [(\mathrm{Fintype}(n))][(\mathrm{DecidableEq}(n))],\forall (u:(n\to \mathbb{C})),\forall (w:(n\to \mathbb{C})),((\mathrm{ketbra}(u,w)){)}^{\ast }=(\mathrm{ketbra}(w,u))$$

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

Source. Repository-derived.

Acknowledgement. Frederik vom Ende (2024). A Sufficient Criterion for Divisibility of Quantum Channels. DOI: 10.1063/5.0231812. URL: https://arxiv.org/html/2407.17103v3.

Commentary.

Taking the adjoint exchanges the two vectors of the rank one operator.

Definition 1.7 (First elementary Kraus operator).

$$\forall (I:\mathrm{Type}),\forall [(\mathrm{Fintype}(I))][(\mathrm{DecidableEq}(I))],\forall (t:\mathbb{R}),\forall (x:(I\to \mathbb{C})),(\mathrm{elementaryK}(t,x))=(1+(((\sqrt{(1-t)}-1))\cdot ((\mathrm{ketbra}(x,x)))))$$

Formalization. D5/S3/Quantum/QuantumChannels/ElementaryChannelDivisibility.elementaryK (✓ std3).

Citation. Frederik vom Ende (2024). A Sufficient Criterion for Divisibility of Quantum Channels. DOI: 10.1063/5.0231812. URL: https://arxiv.org/html/2407.17103v3.

Commentary.

This is Kₜ = I − (1 − √(1−t))|x⟩⟨x| from Definition 1. The real square root is embedded in ℂ.

Definition 1.8 (Second elementary Kraus operator).

$$\forall (I:\mathrm{Type}),\forall [(\mathrm{Fintype}(I))][(\mathrm{DecidableEq}(I))],\forall (t:\mathbb{R}),\forall (x:(I\to \mathbb{C})),\forall (y:(I\to \mathbb{C})),(\mathrm{elementaryL}(t,x,y))=((\sqrt{t})\cdot ((\mathrm{ketbra}(y,x))))$$

Formalization. D5/S3/Quantum/QuantumChannels/ElementaryChannelDivisibility.elementaryL (✓ std3).

Citation. Frederik vom Ende (2024). A Sufficient Criterion for Divisibility of Quantum Channels. DOI: 10.1063/5.0231812. URL: https://arxiv.org/html/2407.17103v3.

Commentary.

This is Lₜ = √t |y⟩⟨x| from Definition 1, with the real coefficient embedded in ℂ.

Definition 1.9 (Elementary channel).

$$\forall (I:\mathrm{Type}),\forall [(\mathrm{Fintype}(I))][(\mathrm{DecidableEq}(I))],\forall (t:\mathbb{R}),\forall (x:(I\to \mathbb{C})),\forall (y:(I\to \mathbb{C})),\forall (X:(\mathrm{Matrix}(I,I,\mathbb{C}))),((\mathrm{elementary}(t,x,y))(X))=((((\mathrm{elementaryK}(t,x))X)((\mathrm{elementaryK}(t,x)){)}^{\ast })+(((\mathrm{elementaryL}(t,x,y))X)((\mathrm{elementaryL}(t,x,y)){)}^{\ast }))$$

Formalization. D5/S3/Quantum/QuantumChannels/ElementaryChannelDivisibility.elementary (✓ std3).

Citation. Frederik vom Ende (2024). A Sufficient Criterion for Divisibility of Quantum Channels. DOI: 10.1063/5.0231812. URL: https://arxiv.org/html/2407.17103v3.

Commentary.

The map is precisely the sum of conjugations by the two source Kraus operators. For an orthogonal unit pair and 0 < t < 1 it is an actual trace-preserving completely positive map.

Definition 1.10 (Exact elementary inverse).

$$\forall (I:\mathrm{Type}),\forall [(\mathrm{Fintype}(I))][(\mathrm{DecidableEq}(I))],\forall (t:\mathbb{R}),\forall (x:(I\to \mathbb{C})),\forall (y:(I\to \mathbb{C})),\forall (X:(\mathrm{Matrix}(I,I,\mathbb{C}))),((\mathrm{elementaryInverse}(t,x,y))(X))=((((1+((((\sqrt{(1-t)}{)}^{-1}-1))\cdot ((\mathrm{ketbra}(x,x)))))X)((1+((((\sqrt{(1-t)}{)}^{-1}-1))\cdot ((\mathrm{ketbra}(x,x))))){)}^{\ast })-((\frac{t}{(1-t)})\cdot ((((\mathrm{ketbra}(y,x))X)((\mathrm{ketbra}(y,x)){)}^{\ast }))))$$

Formalization. D5/S3/Quantum/QuantumChannels/ElementaryChannelDivisibility.elementaryInverse (✓ std3).

Citation. Frederik vom Ende (2024). A Sufficient Criterion for Divisibility of Quantum Channels. DOI: 10.1063/5.0231812. URL: https://arxiv.org/html/2407.17103v3.

Commentary.

Equation (2) defines this linear map. The theorem below proves both inverse identities in its stated range, together with trace preservation on every matrix.

Definition 1.11 (Actual quantum channel).

$$\forall (I:\mathrm{Type}),\forall [(\mathrm{Fintype}(I))][(\mathrm{DecidableEq}(I))],\forall (\varphi :((\mathrm{Matrix}(I,I,\mathbb{C})){\to }_{l[\mathbb{C}]}(\mathrm{Matrix}(I,I,\mathbb{C})))),(((\mathrm{CPTP}(\varphi )))\iff ((((\mathrm{CP}(\varphi )))\wedge (\forall (X:(\mathrm{Matrix}(I,I,\mathbb{C}))),(\mathrm{tr}((\varphi (X))))=(\mathrm{tr}(X))))))$$

Formalization. D5/S3/Quantum/QuantumChannels/ElementaryChannelDivisibility.CPTP (✓ std3).

Source. Repository-derived.

Acknowledgement. Frederik vom Ende (2024). A Sufficient Criterion for Divisibility of Quantum Channels. DOI: 10.1063/5.0231812. URL: https://arxiv.org/html/2407.17103v3.

Commentary.

CP is PhyslibLeaf.MatrixMap.IsCompletelyPositive, rather than positivity only on states or at a bounded amplification. The second conjunct is all-matrix trace preservation.

Definition 1.12 (Elementary right division).

$$\forall (I:\mathrm{Type}),\forall [(\mathrm{Fintype}(I))][(\mathrm{DecidableEq}(I))],\forall (\varphi :((\mathrm{Matrix}(I,I,\mathbb{C})){\to }_{l[\mathbb{C}]}(\mathrm{Matrix}(I,I,\mathbb{C})))),\forall (x:(I\to \mathbb{C})),\forall (y:(I\to \mathbb{C})),(((\mathrm{Divides}(\varphi ,x,y)))\iff (\exists (t:\mathbb{R}),((((0<t)\wedge (t<1)))\wedge ((\mathrm{CP}((\varphi \circ (\mathrm{elementaryInverse}(t,x,y)))))))))$$

Formalization. D5/S3/Quantum/QuantumChannels/ElementaryChannelDivisibility.Divides (✓ std3).

Citation. Frederik vom Ende (2024). A Sufficient Criterion for Divisibility of Quantum Channels. DOI: 10.1063/5.0231812. URL: https://arxiv.org/html/2407.17103v3.

Commentary.

The elementary channel is on the right of the composition. The same ordered pair is retained. The inverse formula is justified by the theorem when the pair is orthogonal and normalized.

Definition 1.13 (Necessary Kraus-space criterion).

$$\forall (I:\mathrm{Type}),\forall [(\mathrm{Fintype}(I))][(\mathrm{DecidableEq}(I))],\forall (J:\mathrm{Type}),\forall [(\mathrm{Fintype}(J))],\forall (K:(J\to (\mathrm{Matrix}(I,I,\mathbb{C})))),\forall (x:(I\to \mathbb{C})),\forall (y:(I\to \mathbb{C})),(((\mathrm{Necessary}(K,x,y)))\iff (\forall (G:(\mathrm{Matrix}(I,I,\mathbb{C}))),((\forall (H:(\mathrm{Matrix}(I,I,\mathbb{C}))),((H\in (\mathrm{span}(\mathbb{C},(\mathrm{range}(K)))))\to ((\mathrm{tr}(((H{)}^{\ast }G)))=0)))\to (\forall (j:J),⟨y,((((K(j)){)}^{\ast }G)(x))⟩=0))))$$

Formalization. D5/S3/Quantum/QuantumChannels/ElementaryChannelDivisibility.Necessary (✓ std3).

Citation. Frederik vom Ende (2024). A Sufficient Criterion for Divisibility of Quantum Channels. DOI: 10.1063/5.0231812. URL: https://arxiv.org/html/2407.17103v3.

Commentary.

Orthogonality is to the complex linear span of the Kraus family. Span induction equates this with tr(Kⱼ*G) = 0 for every Kraus index. The tests range over all complex matrices G and all Kraus indices j. This is Proposition 1’s condition.

Definition 1.14 (Sufficient Kraus-space criterion).

$$\forall (I:\mathrm{Type}),\forall [(\mathrm{Fintype}(I))][(\mathrm{DecidableEq}(I))],\forall (J:\mathrm{Type}),\forall [(\mathrm{Fintype}(J))],\forall (K:(J\to (\mathrm{Matrix}(I,I,\mathbb{C})))),\forall (x:(I\to \mathbb{C})),\forall (y:(I\to \mathbb{C})),(((\mathrm{Sufficient}(K,x,y)))\iff ((((\mathrm{Necessary}(K,x,y)))\wedge (\forall (G:(\mathrm{Matrix}(I,I,\mathbb{C}))),((\forall (H:(\mathrm{Matrix}(I,I,\mathbb{C}))),((H\in (\mathrm{span}(\mathbb{C},(\mathrm{range}(K)))))\to ((\mathrm{tr}(((H{)}^{\ast }G)))=0)))\to (\forall (j:J),⟨x,((((K(j)){)}^{\ast }G)(x))⟩=0))))))$$

Formalization. D5/S3/Quantum/QuantumChannels/ElementaryChannelDivisibility.Sufficient (✓ std3).

Citation. Frederik vom Ende (2024). A Sufficient Criterion for Divisibility of Quantum Channels. DOI: 10.1063/5.0231812. URL: https://arxiv.org/html/2407.17103v3.

Commentary.

Theorem 1 adds the diagonal test ⟨x,Kⱼ*Gx⟩ = 0 to the necessary criterion. Its separate rank-reduction conclusion is not asserted here.

Theorem 1.15 (The exact criterion and failure of the stronger converse).

$$\forall (I:\mathrm{Type}),\forall [(\mathrm{Fintype}(I))][(\mathrm{DecidableEq}(I))],((2\le (\mathrm{card}(I)))\to (((\forall (\varphi :((\mathrm{Matrix}(I,I,\mathbb{C})){\to }_{l[\mathbb{C}]}(\mathrm{Matrix}(I,I,\mathbb{C})))),(((\mathrm{CPTP}(\varphi )))\to (\exists (K:((I\times I)\to (\mathrm{Matrix}(I,I,\mathbb{C})))),\sum _{j\in (I\times I)}(fun(X:(\mathrm{Matrix}(I,I,\mathbb{C})))\mapsto (((K(j))X)((K(j)){)}^{\ast }))=\varphi )))\wedge (\forall (J:\mathrm{Type}),\forall [(\mathrm{Fintype}(J))],\forall (K:(J\to (\mathrm{Matrix}(I,I,\mathbb{C})))),\forall (\varphi :((\mathrm{Matrix}(I,I,\mathbb{C})){\to }_{l[\mathbb{C}]}(\mathrm{Matrix}(I,I,\mathbb{C})))),(((((\mathrm{CPTP}(\varphi )))\wedge (\sum _{j\in J}(fun(X:(\mathrm{Matrix}(I,I,\mathbb{C})))\mapsto (((K(j))X)((K(j)){)}^{\ast }))=\varphi )))\to (\forall (x:(I\to \mathbb{C})),\forall (y:(I\to \mathbb{C})),(((\mathrm{OrthogonalUnitPair}(x,y)))\to ((((\mathrm{Necessary}(K,x,y)))\iff ((\mathrm{Divides}(\varphi ,x,y)))))))))\wedge (\forall (J:\mathrm{Type}),\forall [(\mathrm{Fintype}(J))],\forall (K:(J\to (\mathrm{Matrix}(I,I,\mathbb{C})))),\forall (\varphi :((\mathrm{Matrix}(I,I,\mathbb{C})){\to }_{l[\mathbb{C}]}(\mathrm{Matrix}(I,I,\mathbb{C})))),(((((\mathrm{CPTP}(\varphi )))\wedge (\sum _{j\in J}(fun(X:(\mathrm{Matrix}(I,I,\mathbb{C})))\mapsto (((K(j))X)((K(j)){)}^{\ast }))=\varphi )))\to (((\exists (x:(I\to \mathbb{C})),\exists (y:(I\to \mathbb{C})),(((\mathrm{OrthogonalUnitPair}(x,y)))\wedge ((\mathrm{Necessary}(K,x,y)))))\iff (\exists (x:(I\to \mathbb{C})),\exists (y:(I\to \mathbb{C})),(((\mathrm{OrthogonalUnitPair}(x,y)))\wedge ((\mathrm{Divides}(\varphi ,x,y)))))))))\wedge (\forall (t:\mathbb{R}),((((0<t)\wedge (t<1)))\to (\forall (x:(I\to \mathbb{C})),\forall (y:(I\to \mathbb{C})),(((\mathrm{OrthogonalUnitPair}(x,y)))\to ((((\mathrm{CPTP}((\mathrm{elementary}(t,x,y)))))\wedge (((\mathrm{elementary}(t,x,y))\circ (\mathrm{elementaryInverse}(t,x,y)))=\mathrm{id})\wedge (((\mathrm{elementaryInverse}(t,x,y))\circ (\mathrm{elementary}(t,x,y)))=\mathrm{id})\wedge (\forall (X:(\mathrm{Matrix}(I,I,\mathbb{C}))),(\mathrm{tr}(((\mathrm{elementaryInverse}(t,x,y))(X))))=(\mathrm{tr}(X)))\wedge (\forall (\varphi :((\mathrm{Matrix}(I,I,\mathbb{C})){\to }_{l[\mathbb{C}]}(\mathrm{Matrix}(I,I,\mathbb{C})))),(((((\mathrm{CPTP}(\varphi )))\wedge ((\mathrm{CP}((\varphi \circ (\mathrm{elementaryInverse}(t,x,y))))))))\to ((((\mathrm{CPTP}((\varphi \circ (\mathrm{elementaryInverse}(t,x,y))))))\wedge (((\varphi \circ (\mathrm{elementaryInverse}(t,x,y)))\circ (\mathrm{elementary}(t,x,y)))=\varphi )))))))))))\wedge (\exists (\varphi :((\mathrm{Matrix}(I,I,\mathbb{C})){\to }_{l[\mathbb{C}]}(\mathrm{Matrix}(I,I,\mathbb{C})))),(((\mathrm{CPTP}(\varphi )))\wedge (\exists (x:(I\to \mathbb{C})),\exists (y:(I\to \mathbb{C})),(((\mathrm{OrthogonalUnitPair}(x,y)))\wedge ((\mathrm{Divides}(\varphi ,x,y)))))\wedge (\forall (J:\mathrm{Type}),\forall [(\mathrm{Fintype}(J))],\forall (K:(J\to (\mathrm{Matrix}(I,I,\mathbb{C})))),((\sum _{j\in J}(fun(X:(\mathrm{Matrix}(I,I,\mathbb{C})))\mapsto (((K(j))X)((K(j)){)}^{\ast }))=\varphi )\to (\forall (u:(I\to \mathbb{C})),\forall (v:(I\to \mathbb{C})),(((\mathrm{OrthogonalUnitPair}(u,v)))\to (\neg (\mathrm{Sufficient}(K,u,v))))))))))))$$

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

Resolves. Problems/vomende-2024-elementary-channel-divisibility (proved) by D5/S3/Quantum/QuantumChannels/ElementaryChannelDivisibility.result.

Source. Repository-derived.

Acknowledgement. Frederik vom Ende (2024). A Sufficient Criterion for Divisibility of Quantum Channels. DOI: 10.1063/5.0231812. URL: https://arxiv.org/html/2407.17103v3.

Commentary.

Every actual CPTP map has a finite Kraus representation. For every finite dimension at least two, the necessary criterion is equivalent to elementary division for the same ordered pair, and therefore also after existential quantification over pairs. These equivalences hold for every finite Kraus representation of an actual CPTP map. The last conjunct exhibits an actual CPTP map with an elementary division and no pair satisfying the stronger sufficient criterion, in every representation. Thus neither the fixed-pair nor the existential-pair converse of that sufficient criterion holds. The Proved resolution marker records this combined classification: both necessary-criterion equivalences are proved, while both assertions that elementary division implies the stronger sufficient criterion are refuted.

In input-first Choi coordinates let A = C(Φ) and Z = (|y⟩⟨x|)ᵀ ⊗ I. Hilbert–Schmidt orthogonality identifies the tests with ker A ⊆ ker(ZA Z*). If this inclusion holds, square roots factor as √B = C√A for B = ZA Z*. The operator norm bound gives B ≤ ‖C‖²A, and t = 1/(2(‖C‖²+1)) gives A−tB ≥ 0, including singular A. The exact Choi matrix of the residual is D(A−tB)D*, where D = Rᵀ ⊗ I and R is the inverse filter. Its congruence is invertible for 0 < t < 1.

For distinct basis vectors eᵣ,eₛ, take Φ = elementary(15/16,eᵣ,eₛ) and Q = elementary(3/4,eᵣ,eₛ). Direct Kraus algebra gives Q∘Q = Φ, hence Φ∘Q⁻¹ = Q. For any unit u, the diagonal sufficient test fails: the Hilbert–Schmidt tests Eᵣᵢ for i ≠ r force either uᵣ = 0 or all other coordinates to vanish, while a diagonal orthogonal test gives 1−|I||uᵣ|² = 0. Both alternatives contradict normalization when |I| ≥ 2. The intrinsic kernel criterion transfers this obstruction to every finite Kraus representation. These are finite-dimensional conclusions; no dimension-one pair or infinite-dimensional domination statement is included.

References

• Truth anchor: D5/S3/Quantum/QuantumChannels/ElementaryChannelDivisibility.CPTP
• Truth anchor: D5/S3/Quantum/QuantumChannels/ElementaryChannelDivisibility.Divides
• Truth anchor: D5/S3/Quantum/QuantumChannels/ElementaryChannelDivisibility.Necessary
• Truth anchor: D5/S3/Quantum/QuantumChannels/ElementaryChannelDivisibility.OrthogonalUnitPair
• Truth anchor: D5/S3/Quantum/QuantumChannels/ElementaryChannelDivisibility.Sufficient
• Truth anchor: D5/S3/Quantum/QuantumChannels/ElementaryChannelDivisibility.basis_pair
• Truth anchor: D5/S3/Quantum/QuantumChannels/ElementaryChannelDivisibility.elementary
• Truth anchor: D5/S3/Quantum/QuantumChannels/ElementaryChannelDivisibility.elementaryInverse
• Truth anchor: D5/S3/Quantum/QuantumChannels/ElementaryChannelDivisibility.elementaryK
• Truth anchor: D5/S3/Quantum/QuantumChannels/ElementaryChannelDivisibility.elementaryL
• Truth anchor: D5/S3/Quantum/QuantumChannels/ElementaryChannelDivisibility.factor_of_kernel
• Truth anchor: D5/S3/Quantum/QuantumChannels/ElementaryChannelDivisibility.kernel_of_sub_psd
• Truth anchor: D5/S3/Quantum/QuantumChannels/ElementaryChannelDivisibility.ketbra
• Truth anchor: D5/S3/Quantum/QuantumChannels/ElementaryChannelDivisibility.ketbra_star
• Truth anchor: D5/S3/Quantum/QuantumChannels/ElementaryChannelDivisibility.result
• Dependency: D5/S3/Quantum/Recovery/ActualChannelAlgebra