Hildebrand sufficiency on two qutrits

Abstract

The two Hildebrand pencils characterize absolutely PPT density matrices on two qutrits.

Theorem 1.1 (Ordered spectral necessity).

$\forall (k : N), \forall (r h o : M a t r i x ((F in (3) \times F in (3 + k)), (F in (3) \times F in (3 + k)), C)), \forall (h r h o : (r h o) . P os S e mi d e f), (((r h o) . t r a ce = 1) \land (A PPT (r h o))) \Rightarrow (\exists (l : F in (3 \cdot (3 + k)) \to R), (A n t i t o n e (l)) \land (\forall (i : F in (3 \cdot (3 + k))), 0 \leq l (i)) \land (i : F in (3 \cdot (3 + k)) \sum l (i) = 1) \land ((K 1 (b o u n d a ry Va l u es (k, l))) . P os S e mi d e f) \land ((K 2 (b o u n d a ry Va l u es (k, l))) . P os S e mi d e f) \land (((r h o \cdot r h o) . t r a ce) . re = i : F in (3 \cdot (3 + k)) \sum (l (i))^{2}) \land (l = (f u n (i : F in (3 \cdot (3 + k))) \mapsto h r h o . i sHer mi t ian . e i g e n v a l u e s_{0} (F in . c a s t (i)))))$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsolutePPT/QutritHildebrandSufficiency.spectral_reduction_ordered (✓ std3). ∎

Citation. Roland Hildebrand (2007). Positive partial transpose from spectra. DOI: 10.1103/PhysRevA.76.052325. URL: https://arxiv.org/abs/quant-ph/0502170.

Commentary.

The eigenvalues are the sorted eigenvalues chosen in the spectral reduction. The proof argument of Fin.cast is omitted; it is the cardinality equality for Fin 3 × Fin (3+k).

Theorem 1.2 (Spectrum as an ordered range).

$\forall (k : N), \forall (r h o : M a t r i x ((F in (3) \times F in (3 + k)), (F in (3) \times F in (3 + k)), C)), \forall (H : M a t r i x . I sHer mi t ian (r h o)), s p ec t r u m (C, r h o) = S e t . ima g e (C o m pl e x . o f R e a l, S e t . r an g e ((f u n (i : F in (3 \cdot (3 + k))) \mapsto H . e i g e n v a l u e s_{0} (F in . c a s t (i)))))$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsolutePPT/QutritHildebrandSufficiency.spectrum_eq_ordered_range (✓ std3). ∎

Source. Repository-derived.

Commentary.

The complex spectrum is the real embedding of the range of the sorted eigenvalues. The proof argument of Fin.cast is omitted; it is the cardinality equality for Fin 3 × Fin (3+k).

Theorem 1.3 (Trace and squared unitary entries).

$\forall (I : T y p e), [F in t y p e (I)] [Dec i d ab l e Eq (I)] \forall (w : I \to R), \forall (l : I \to R), \forall (U : u ni t a ry G ro u p (I, C)), ((M a t r i x . d ia g o na l ((f u n (i : I) \mapsto (w (i) : C))) \cdot (U : M a t r i x (I, I, C)) \cdot M a t r i x . d ia g o na l ((f u n (i : I) \mapsto (l (i) : C))) \cdot M a t r i x . co nj T r an s p ose ((U : M a t r i x (I, I, C)))) . t r a ce) . re = i : I \sum j : I \sum w (i) \cdot R H L ina l g . n or m SqM a t r i x ((U : M a t r i x (I, I, C)), i, j) \cdot l (j)$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsolutePPT/QutritHildebrandSufficiency.trace_diagonal_conjugate (✓ std3). ∎

Source. Repository-derived.

Commentary.

Expansion of the trace gives the finite sum with squared moduli of the unitary entries.

Theorem 1.4 (Trace lower bound).

$\forall (I : T y p e), [F in t y p e (I)] [Dec i d ab l e Eq (I)] \forall (w : I \to R), \forall (l : I \to R), \forall (U : u ni t a ry G ro u p (I, C)), (M o n o v a ry ((f u n (i : I) \mapsto - w (i)), l)) \Rightarrow (i : I \sum w (i) \cdot l (i) \leq ((M a t r i x . d ia g o na l ((f u n (i : I) \mapsto (w (i) : C))) \cdot (U : M a t r i x (I, I, C)) \cdot M a t r i x . d ia g o na l ((f u n (i : I) \mapsto (l (i) : C))) \cdot M a t r i x . co nj T r an s p ose ((U : M a t r i x (I, I, C)))) . t r a ce) . re)$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsolutePPT/QutritHildebrandSufficiency.trace_lower_of_monovary_diagonalization (✓ std3). ∎

Source. Repository-derived.

Commentary.

Oppositely ordered weights give a lower bound for the trace of the conjugated diagonal operator.

Theorem 1.5 (Sorted diagonalization).

$\forall (I : T y p e), [F in t y p e (I)] [Dec i d ab l e Eq (I)] \forall (n : N), \forall (h c : F in t y p e . c a r d (I) = n), \forall (A : M a t r i x (I, I, C)), \forall (H : M a t r i x . I sHer mi t ian (A)), \forall (e : Eq u i v (I, F in (n))), \exists (U : u ni t a ry G ro u p (I, C)), A = (U : M a t r i x (I, I, C)) \cdot M a t r i x . d ia g o na l ((f u n (i : I) \mapsto ((f u n (i : F in (n)) \mapsto H . e i g e n v a l u e s_{0} (F in . c a s t (h c . sy mm, i))) (e (i)) : C))) \cdot M a t r i x . co nj T r an s p ose ((U : M a t r i x (I, I, C)))$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsolutePPT/QutritHildebrandSufficiency.sorted_diagonalization (✓ std3). ∎

Source. Repository-derived.

Commentary.

A unitary conjugates the diagonal matrix indexed by the chosen equivalence to the Hermitian matrix.

Theorem 1.6 (Descending eigenvalues).

$\forall (J : T y p e), [F in t y p e (J)] [Dec i d ab l e Eq (J)] \forall (n : N), \forall (h c : F in t y p e . c a r d (J) = n), \forall (A : M a t r i x (J, J, C)), \forall (H : M a t r i x . I sHer mi t ian (A)), A n t i t o n e ((f u n (i : F in (n)) \mapsto H . e i g e n v a l u e s_{0} (F in . c a s t (h c . sy mm, i))))$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsolutePPT/QutritHildebrandSufficiency.sorted_eigenvalues_antitone (✓ std3). ∎

Source. Repository-derived.

Commentary.

Reindexing by the cardinality equality preserves descending order.

Theorem 1.7 (Hildebrand sufficiency).

$\forall (r h o : M a t r i x ((F in (3) \times F in (3)), (F in (3) \times F in (3)), C)), \forall (H : M a t r i x . I sHer mi t ian (r h o)), (((K 1 ((f u n (i : F in (9)) \mapsto H . e i g e n v a l u e s_{0} (F in . c a s t (i))))) . P os S e mi d e f) \land ((K 2 ((f u n (i : F in (9)) \mapsto H . e i g e n v a l u e s_{0} (F in . c a s t (i))))) . P os S e mi d e f)) \Rightarrow (A PPT (r h o))$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsolutePPT/QutritHildebrandSufficiency.hildebrand_sufficiency (✓ std3). ∎

Citation. Roland Hildebrand (2007). Positive partial transpose from spectra. DOI: 10.1103/PhysRevA.76.052325. URL: https://arxiv.org/abs/quant-ph/0502170.

Commentary.

Positivity of both real pencils implies positivity of every partial transpose after unitary conjugation. Hildebrand, Corollary 4, pages 5–6. Fin.cast omits the proof of the carrier cardinality equality.

Theorem 1.8 (Two-qutrit boundary coordinates).

$\forall (l : F in (9) \to R), b o u n d a ry Va l u es (0, l) = l$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsolutePPT/QutritHildebrandSufficiency.boundary_values_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

When both local dimensions are three, all nine boundary coordinates are unchanged.

Theorem 1.9 (Hildebrand equivalence).

$\forall (r h o : M a t r i x ((F in (3) \times F in (3)), (F in (3) \times F in (3)), C)), \forall (h p : (r h o) . P os S e mi d e f), ((r h o) . t r a ce = 1) \Rightarrow (A PPT (r h o) ⟺ ((K 1 ((f u n (i : F in (9)) \mapsto h p . i sHer mi t ian . e i g e n v a l u e s_{0} (F in . c a s t (i))))) . P os S e mi d e f) \land ((K 2 ((f u n (i : F in (9)) \mapsto h p . i sHer mi t ian . e i g e n v a l u e s_{0} (F in . c a s t (i))))) . P os S e mi d e f))$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsolutePPT/QutritHildebrandSufficiency.hildebrand_criterion (✓ std3). ∎

Citation. Roland Hildebrand (2007). Positive partial transpose from spectra. DOI: 10.1103/PhysRevA.76.052325. URL: https://arxiv.org/abs/quant-ph/0502170.

Commentary.

For a positive trace-one matrix, absolute PPT is equivalent to positivity of both Hildebrand pencils. Hildebrand, Corollary 4, pages 5–6. Fin.cast omits the proof of the carrier cardinality equality.

Theorem 1.10 (Identification of sorted diagonal entries).

$\forall (J : T y p e), [F in t y p e (J)] [Dec i d ab l e Eq (J)] \forall (n : N), \forall (h c : F in t y p e . c a r d (J) = n), \forall (A : M a t r i x (J, J, C)), \forall (H : M a t r i x . I sHer mi t ian (A)), \forall (l : F in (n) \to R), \forall (e : Eq u i v (J, F in (n))), \forall (U : u ni t a ry G ro u p (J, C)), ((A n t i t o n e (l)) \land (A = (U : M a t r i x (J, J, C)) \cdot M a t r i x . d ia g o na l ((f u n (i : J) \mapsto (l (e (i)) : C))) \cdot M a t r i x . co nj T r an s p ose ((U : M a t r i x (J, J, C))))) \Rightarrow ((f u n (i : F in (n)) \mapsto H . e i g e n v a l u e s_{0} (F in . c a s t (h c . sy mm, i))) = l)$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsolutePPT/QutritHildebrandSufficiency.sorted_eigenvalues_of_diagonalization (✓ std3). ∎

Source. Repository-derived.

Commentary.

An antitone diagonal list in a unitary diagonalization equals the sorted eigenvalues.

trureturing — Discovering truth

Hildebrand sufficiency on two qutrits

Abstract

References

Keyboard shortcuts

trureturing — Discovering truth

Hildebrand sufficiency on two qutrits

Abstract

References