Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

An extreme POVM with rank vector (3,3,2,2,2,2,2,2)

Abstract

An explicit extreme eight-outcome POVM on complex seven-space refutes the proposed rank-vector exclusion.

Definition 1.1 (Midpoint extremality of a finite POVM).

Formalization. D5/S3/Quantum/Measurement/ExtremePOVMRankThreeThreeTwoSix.IsExtreme (✓ std3).

Citation. Erkka Haapasalo; Juha-Pekka Pellonpää (2020). Effective methods for constructing extreme quantum observables. DOI: 10.1088/1751-8121/ab8d52. URL: https://arxiv.org/abs/1809.09935v1.

Commentary.

An n-outcome family of complex 7 by 7 matrices is extreme when it is a POVM and every midpoint decomposition into two POVMs has both factors equal to the original family. This is the midpoint formulation of extremality in Haapasalo and Pellonpää, lines 148–152.

Definition 1.2 (Ranks after omitting rank-one outcomes).

Formalization. D5/S3/Quantum/Measurement/ExtremePOVMRankThreeThreeTwoSix.bigRanks (✓ std3).

Citation. Erkka Haapasalo; Juha-Pekka Pellonpää (2020). Effective methods for constructing extreme quantum observables. DOI: 10.1088/1751-8121/ab8d52. URL: https://arxiv.org/abs/1809.09935v1.

Commentary.

bigRanks maps the finite outcome index set to the natural ranks of the effects and filters out all ranks below two. It is the multiset form of the source’s rank vector convention, which orders ranks with repetition and omits rank-one outcomes (lines 219–222).

Definition 1.3 (The proposed rank-vector exclusion).

Formalization. D5/S3/Quantum/Measurement/ExtremePOVMRankThreeThreeTwoSix.claim (✓ std3).

Source. Repository-derived.

Acknowledgement. Erkka Haapasalo; Juha-Pekka Pellonpää (2020). Effective methods for constructing extreme quantum observables. DOI: 10.1088/1751-8121/ab8d52. URL: https://arxiv.org/abs/1809.09935v1.

Commentary.

The formal claim says that every extreme finite POVM on complex seven-space has a big-rank multiset different from two rank-three effects followed by six rank-two effects. This is the negative existence question for the problematic vector (3₂,2₆)₇ named in the source at lines 307–314.

Theorem 1.4 (An explicit counterexample to the exclusion).

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

Resolves. Problems/haapasalo-pellonpaa-2020-extreme-povm-rank-vector-three-three-two-six (refuted) by D5/S3/Quantum/Measurement/ExtremePOVMRankThreeThreeTwoSix.result.

Source. Repository-derived.

Acknowledgement. Erkka Haapasalo; Juha-Pekka Pellonpää (2020). Effective methods for constructing extreme quantum observables. DOI: 10.1088/1751-8121/ab8d52. URL: https://arxiv.org/abs/1809.09935v1.

Commentary.

The construction uses the ordered coordinates (e₀,e₁,e₂,f₀,f₁,f₂,g) of complex seven-space. Eight blocks of vectors are formed: two coordinate blocks consisting of the three e coordinates and the three f coordinates, and six phase blocks with phase-zero and phase-i choices for each of the three pairs of e coordinates. Four of the six phase blocks contain the apex coordinate g. For each block, form the positive matrix effect j by summing b bᴴ over its vectors, and let frame be the sum of all eight effects.

Lean’s frame_posDef lemma proves positive definiteness of frame using its positive-semidefinite sum decomposition and an exact coordinate calculation showing that its matrix-vector action is injective. The positive square-root factorization of a strictly positive matrix then supplies an invertible normalizer with normalizer · frame · normalizerᴴ = 1. Conjugating every effect by this normalizer gives witness; congruence preserves positive semidefiniteness, the conjugated effects sum to the identity, and congruence by an invertible matrix preserves rank.

The block-column factorization effect j = columns j · (columns j)ᴴ identifies each effect rank with the cardinality of its block. The two coordinate blocks have cardinality three and the other six blocks cardinality two, so witness has bigRanks equal to the target multiset. For each block, an explicit left inverse of its columns is verified by finite coordinate cases. Expanding the conjugated products therefore reduces independence to the 42 within-block products, whose coefficients are separated by the two phase choices, the apex coordinates, and the coordinate blocks.

For a midpoint decomposition of witness into POVMs A and B, positivity and the midpoint equation imply that each difference A j − witness j lies in the span of the outer products of the normalized columns (the normalizer applied to the columns of block j). The left inverse gives a coefficient matrix for this difference, and the normalized expansion expresses it as a linear combination of the independent 42 conjugated within-block products. Summing over j gives zero because both families sum to the identity, so every coefficient vanishes. Thus A = witness, and the midpoint equation then gives B = witness. Hence witness is extreme and its target big-rank multiset contradicts claim at n = 8.

References