A quantum behavior with rank of contextuality three

Abstract

A quantum behavior has rank of contextuality three.

Fin n consists of the n labels starting at zero. A context C(x) is an ordered list of observable labels; its outcome is a function Fin (List.length (C(x))) → Bool. The bit true means eigenvalue −1. Behavior is the real table carrier; IsQuantum supplies the quantum probabilities. The real weights mu correspond to μ and the matrix rho to ρ. All matrix traces are complex traces; ofReal explicitly embeds each real probability into Complex. Finite sets count distinct behaviors, rather than labels of models that happen to agree.

Definition 1.1 (Behavior tables).

$$\forall (k:Nat),\forall (m:Nat),\forall (C:(Fin\left(k\right)\to List\left(Fin\left(m\right)\right))),Behavior\left(C\right)=(x:Fin\left(k\right))\to ((Fin\left(\mathrm{List}.\mathrm{length}\left(C\left(x\right)\right)\right)\to Bool)\to Real)$$

Formalization. D5/S3/QuantumContext/RankOfContextualityNonPowerTwo.Behavior (✓ std3).

Source. Repository-derived.

Acknowledgement. K. Horodecki; J. Zhou; M. Stankiewicz; R. Salazar; P. Horodecki; R. Raussendorf; R. Horodecki; R. Ramanathan; E. Tyhurst (2022). The rank of contextuality. DOI: 10.1088/1367-2630/acdf78. URL: https://arxiv.org/abs/2205.10307.

Commentary.

The carrier consists of real-valued tables indexed by contexts and outcomes, on which IsQuantum and NonContextual impose the source’s probability conditions.

Definition 1.2 (Restriction of a global assignment).

$$\forall (k:Nat),\forall (m:Nat),\forall (C:(Fin\left(k\right)\to List\left(Fin\left(m\right)\right))),\forall (x:Fin\left(k\right)),\forall (g:(Fin\left(m\right)\to Bool)),restrict\left(C,x,g\right)=fun(i:Fin\left(\mathrm{List}.\mathrm{length}\left(C\left(x\right)\right)\right))\mapsto g\left(\mathrm{List}.\mathrm{get}\left(C\left(x\right),i\right)\right)$$

Formalization. D5/S3/QuantumContext/RankOfContextualityNonPowerTwo.restrict (✓ std3).

Citation. K. Horodecki; J. Zhou; M. Stankiewicz; R. Salazar; P. Horodecki; R. Raussendorf; R. Horodecki; R. Ramanathan; E. Tyhurst (2022). The rank of contextuality. DOI: 10.1088/1367-2630/acdf78. URL: https://arxiv.org/abs/2205.10307.

Commentary.

Section 2, PDF page 4: “We refer to output A given input X as an ordered list of outcomes (a₁, a₂, . . . , a|X|)), that is, it assigns a value to every observable in the context corresponding to X.” The i-th output is the predetermined value of the observable at position i in C(x).

Definition 1.3 (Noncontextual distributions).

$$\forall (k:Nat),\forall (m:Nat),\forall (C:(Fin\left(k\right)\to List\left(Fin\left(m\right)\right))),\forall (N:Behavior\left(C\right)),NonContextual\left(C,N\right)⟺\exists (mu:((Fin\left(m\right)\to Bool)\to Real)),(\forall (g:(Fin\left(m\right)\to Bool)),0\le mu\left(g\right))\wedge ((\sum _{g:(Fin\left(m\right)\to Bool)}mu\left(g\right)=1)\wedge (\forall (x:Fin\left(k\right)),\forall (a:(Fin\left(\mathrm{List}.\mathrm{length}\left(C\left(x\right)\right)\right)\to Bool)),N\left(x,a\right)=\sum _{g:(Fin\left(m\right)\to Bool)withrestrict\left(C,x,g\right)=a}mu\left(g\right)))$$

Formalization. D5/S3/QuantumContext/RankOfContextualityNonPowerTwo.NonContextual (✓ std3).

Citation. K. Horodecki; J. Zhou; M. Stankiewicz; R. Salazar; P. Horodecki; R. Raussendorf; R. Horodecki; R. Ramanathan; E. Tyhurst (2022). The rank of contextuality. DOI: 10.1088/1367-2630/acdf78. URL: https://arxiv.org/abs/2205.10307.

Commentary.

Section 2, PDF page 4, equation (2): “In other words: a non-contextual behavior PNC is a probabilistic mixture of deterministic behaviors that have fixed values of outcomes to any observable beforehand.” The weight mu is nonnegative and has total mass one. The fiber sum is over all assignments g whose restriction equals a.

Definition 1.4 (Cardinalities of noncontextual covers).

$$\forall (k:Nat),\forall (m:Nat),\forall (C:(Fin\left(k\right)\to List\left(Fin\left(m\right)\right))),\forall (P:Behavior\left(C\right)),coverSizes\left(C,P\right)=\{n:Nat\mid \exists (S:Finset\left(Behavior\left(C\right)\right)),(\mathrm{Finset}.\mathrm{card}\left(S\right)=n)\wedge ((\forall (N:Behavior\left(C\right)),N\in S⟹NonContextual\left(C,N\right))\wedge (\forall (x:Fin\left(k\right)),\exists (N:Behavior\left(C\right)),(N\in S)\wedge (\forall (a:(Fin\left(\mathrm{List}.\mathrm{length}\left(C\left(x\right)\right)\right)\to Bool)),N\left(x,a\right)=P\left(x,a\right))))\}$$

Formalization. D5/S3/QuantumContext/RankOfContextualityNonPowerTwo.coverSizes (✓ std3).

Citation. K. Horodecki; J. Zhou; M. Stankiewicz; R. Salazar; P. Horodecki; R. Raussendorf; R. Horodecki; R. Ramanathan; E. Tyhurst (2022). The rank of contextuality. DOI: 10.1088/1367-2630/acdf78. URL: https://arxiv.org/abs/2205.10307.

Commentary.

Definition 3.1, PDF page 5: “Let P be a behavior. Let N be the set of all non-contextual behaviors, each of the form Nᵢ(A | X). Then we define the rank of contextuality denoted as RC in the following way” “where |S| denotes the cardinality of the set S.” A single member must reproduce all outcomes at a given context; the member may depend on the context.

Definition 1.5 (The least cover cardinality).

$$\forall (k:Nat),\forall (m:Nat),\forall (C:(Fin\left(k\right)\to List\left(Fin\left(m\right)\right))),\forall (P:Behavior\left(C\right)),\forall (r:Nat),IsRankOfContextuality\left(C,P,r\right)⟺IsLeast\left(coverSizes\left(C,P\right),r\right)$$

Formalization. D5/S3/QuantumContext/RankOfContextualityNonPowerTwo.IsRankOfContextuality (✓ std3).

Citation. K. Horodecki; J. Zhou; M. Stankiewicz; R. Salazar; P. Horodecki; R. Raussendorf; R. Horodecki; R. Ramanathan; E. Tyhurst (2022). The rank of contextuality. DOI: 10.1088/1367-2630/acdf78. URL: https://arxiv.org/abs/2205.10307.

Commentary.

Definition 3.1, PDF page 5, equation (3): “Let P be a behavior. Let N be the set of all non-contextual behaviors, each of the form Nᵢ(A | X). Then we define the rank of contextuality denoted as RC in the following way” “where |S| denotes the cardinality of the set S.” IsLeast expresses membership and the lower bound on every cover cardinality.

Definition 1.6 (Quantum realization).

$$\forall (k:Nat),\forall (m:Nat),\forall (C:(Fin\left(k\right)\to List\left(Fin\left(m\right)\right))),\forall (P:Behavior\left(C\right)),IsQuantum\left(C,P\right)⟺\exists (d:Nat),\exists (rho:Matrix\left(Fin\left(d\right),Fin\left(d\right),Complex\right)),\exists (O:(Fin\left(m\right)\to Matrix\left(Fin\left(d\right),Fin\left(d\right),Complex\right))),(\mathrm{Matrix}.\mathrm{PosSemidef}\left(rho\right))\wedge ((\mathrm{Matrix}.\mathrm{trace}\left(rho\right)=1)\wedge ((\forall (v:Fin\left(m\right)),(\mathrm{Matrix}.\mathrm{IsHermitian}\left(O\left(v\right)\right))\wedge ((O\left(v\right))\cdot (O\left(v\right))=1))\wedge ((\forall (x:Fin\left(k\right)),\forall (i:Fin\left(\mathrm{List}.\mathrm{length}\left(C\left(x\right)\right)\right)),\forall (j:Fin\left(\mathrm{List}.\mathrm{length}\left(C\left(x\right)\right)\right)),Commute\left(O\left(\mathrm{List}.\mathrm{get}\left(C\left(x\right),i\right)\right),O\left(\mathrm{List}.\mathrm{get}\left(C\left(x\right),j\right)\right)\right))\wedge (\forall (x:Fin\left(k\right)),\forall (a:(Fin\left(\mathrm{List}.\mathrm{length}\left(C\left(x\right)\right)\right)\to Bool)),\mathrm{Complex}.\mathrm{ofReal}\left(P\left(x,a\right)\right)=\mathrm{Matrix}.\mathrm{trace}\left((rho)\cdot (\mathrm{List}.\mathrm{prod}\left(\mathrm{List}.\mathrm{ofFn}\left(fun(i:Fin\left(\mathrm{List}.\mathrm{length}\left(C\left(x\right)\right)\right))\mapsto \mathrm{HSMul}.\mathrm{hSMul}\left((\frac{1}{2}:Complex),1+\mathrm{HSMul}.\mathrm{hSMul}\left((ifa\left(i\right)then-1else1:Complex),O\left(\mathrm{List}.\mathrm{get}\left(C\left(x\right),i\right)\right)\right)\right)\right)\right))\right)))))$$

Formalization. D5/S3/QuantumContext/RankOfContextualityNonPowerTwo.IsQuantum (✓ std3).

Citation. K. Horodecki; J. Zhou; M. Stankiewicz; R. Salazar; P. Horodecki; R. Raussendorf; R. Horodecki; R. Ramanathan; E. Tyhurst (2022). The rank of contextuality. DOI: 10.1088/1367-2630/acdf78. URL: https://arxiv.org/abs/2205.10307.

Commentary.

Section 2, PDF page 4: “With any set of observables V = {Vᵢ}, we can identify their commutation relations and represent them by a hypergraph H on this set where hyperedges are subsets of the powerset of V that denote contexts, i.e. sets of mutually commuting observables.” Binary observables are Hermitian involutions. Their spectral projections are multiplied in the list order, and the Born probability is the trace against the density matrix.

Definition 1.7 (The construction question).

$$claim⟺\exists (m:Nat),\exists (k:Nat),\exists (C:(Fin\left(k\right)\to List\left(Fin\left(m\right)\right))),\exists (P:Behavior\left(C\right)),\exists (r:Nat),(IsQuantum\left(C,P\right))\wedge ((IsRankOfContextuality\left(C,P,r\right))\wedge (\forall (n:Nat),r\ne 2^n))$$

Formalization. D5/S3/QuantumContext/RankOfContextualityNonPowerTwo.claim (✓ std3).

Citation. K. Horodecki; J. Zhou; M. Stankiewicz; R. Salazar; P. Horodecki; R. Raussendorf; R. Horodecki; R. Ramanathan; E. Tyhurst (2022). The rank of contextuality. DOI: 10.1088/1367-2630/acdf78. URL: https://arxiv.org/abs/2205.10307.

Commentary.

Section 9 (Section IX in the arXiv source), PDF page 19: “Finally, it would be interesting to construct a quantum behavior having the rank of contextuality different from the power of 2 (the power of 2 is achieved by a tensor product of the Peres-Mermin behaviors).” The observable and context counts m and k, their lists C, the behavior P and its integer rank r are all existential. The final universal quantifier excludes every power 2^n, including n = 0.

Definition 1.8 (The square’s row and column indices).

$$((\mathrm{Square}.\mathrm{idx}\left(0,0\right)=0)\wedge ((\mathrm{Square}.\mathrm{idx}\left(0,1\right)=1)\wedge ((\mathrm{Square}.\mathrm{idx}\left(0,2\right)=2)\wedge ((\mathrm{Square}.\mathrm{idx}\left(1,0\right)=3)\wedge ((\mathrm{Square}.\mathrm{idx}\left(1,1\right)=4)\wedge ((\mathrm{Square}.\mathrm{idx}\left(1,2\right)=5)\wedge ((\mathrm{Square}.\mathrm{idx}\left(2,0\right)=6)\wedge ((\mathrm{Square}.\mathrm{idx}\left(2,1\right)=7)\wedge ((\mathrm{Square}.\mathrm{idx}\left(2,2\right)=8)\wedge ((\mathrm{Square}.\mathrm{idx}\left(3,0\right)=0)\wedge ((\mathrm{Square}.\mathrm{idx}\left(3,1\right)=3)\wedge ((\mathrm{Square}.\mathrm{idx}\left(3,2\right)=6)\wedge ((\mathrm{Square}.\mathrm{idx}\left(4,0\right)=1)\wedge ((\mathrm{Square}.\mathrm{idx}\left(4,1\right)=4)\wedge ((\mathrm{Square}.\mathrm{idx}\left(4,2\right)=7)\wedge ((\mathrm{Square}.\mathrm{idx}\left(5,0\right)=2)\wedge ((\mathrm{Square}.\mathrm{idx}\left(5,1\right)=5)\wedge (\mathrm{Square}.\mathrm{idx}\left(5,2\right)=8))))))))))))))))))\wedge (\forall (x:Fin\left(6\right)),(\mathrm{Square}.C\left(x\right):List\left(Fin\left(9\right)\right))=\mathrm{List}.\mathrm{cons}\left(\mathrm{Square}.\mathrm{idx}\left(x,0\right),\mathrm{List}.\mathrm{cons}\left(\mathrm{Square}.\mathrm{idx}\left(x,1\right),\mathrm{List}.\mathrm{cons}\left(\mathrm{Square}.\mathrm{idx}\left(x,2\right),\mathrm{List}.\mathrm{nil}\right)\right)\right))$$

Formalization. D5/S3/QuantumContext/RankOfContextualityNonPowerTwo.idx (✓ std3).

Source. Repository-derived.

Acknowledgement. K. Horodecki; J. Zhou; M. Stankiewicz; R. Salazar; P. Horodecki; R. Raussendorf; R. Horodecki; R. Ramanathan; E. Tyhurst (2022). The rank of contextuality. DOI: 10.1088/1367-2630/acdf78. URL: https://arxiv.org/abs/2205.10307.

Commentary.

The eighteen equations list all three positions of each of the six contexts. Labels zero through eight are in row-major order; the first three contexts are rows and the last three are columns. The ordered context C(x) is the list of these three indices.

Definition 1.9 (The parity of three binary outcomes).

$$\forall (a:(Fin\left(3\right)\to Bool)),\mathrm{Square}.parity3\left(a\right)=\mathrm{Bool}.\mathrm{xor}\left(\mathrm{Bool}.\mathrm{xor}\left(a\left(0\right),a\left(1\right)\right),a\left(2\right)\right)$$

Formalization. D5/S3/QuantumContext/RankOfContextualityNonPowerTwo.parity3 (✓ std3).

Source. Repository-derived.

Acknowledgement. K. Horodecki; J. Zhou; M. Stankiewicz; R. Salazar; P. Horodecki; R. Raussendorf; R. Horodecki; R. Ramanathan; E. Tyhurst (2022). The rank of contextuality. DOI: 10.1088/1367-2630/acdf78. URL: https://arxiv.org/abs/2205.10307.

Commentary.

Exclusive-or of the three outcomes records whether an odd number are true.

Definition 1.10 (The square’s prescribed context parities).

$$\forall (x:Fin\left(6\right)),\mathrm{Square}.\mathrm{target}\left(x\right)=ite\left(x=5,\mathrm{Bool}.\mathrm{true},\mathrm{Bool}.\mathrm{false}\right)$$

Formalization. D5/S3/QuantumContext/RankOfContextualityNonPowerTwo.target (✓ std3).

Source. Repository-derived.

Acknowledgement. K. Horodecki; J. Zhou; M. Stankiewicz; R. Salazar; P. Horodecki; R. Raussendorf; R. Horodecki; R. Ramanathan; E. Tyhurst (2022). The rank of contextuality. DOI: 10.1088/1367-2630/acdf78. URL: https://arxiv.org/abs/2205.10307.

Commentary.

Only context five, the third column, has target true, corresponding to a negative product.

Lemma 1.11 (Parity as a natural-number residue).

$$\forall (a:(Fin\left(3\right)\to Bool)),\mathrm{Bool}.\mathrm{toNat}\left(\mathrm{Square}.parity3\left(a\right)\right)=\mathrm{Nat}.\mathrm{mod}\left(\mathrm{Bool}.\mathrm{toNat}\left(a\left(0\right)\right)+\mathrm{Bool}.\mathrm{toNat}\left(a\left(1\right)\right)+\mathrm{Bool}.\mathrm{toNat}\left(a\left(2\right)\right),2\right)$$

Proof. Machine-checked in Lean as D5/S3/QuantumContext/RankOfContextualityNonPowerTwo.bv_parity (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. K. Horodecki; J. Zhou; M. Stankiewicz; R. Salazar; P. Horodecki; R. Raussendorf; R. Horodecki; R. Ramanathan; E. Tyhurst (2022). The rank of contextuality. DOI: 10.1088/1367-2630/acdf78. URL: https://arxiv.org/abs/2205.10307.

Commentary.

The natural value of the Boolean parity is the sum of the three natural bit values modulo two.

Lemma 1.12 (Every assignment misses a square parity).

$$\forall (g:(Fin\left(9\right)\to Bool)),\exists (x:Fin\left(6\right)),\mathrm{Square}.parity3\left(fun(i:Fin\left(3\right))\mapsto g\left(\mathrm{List}.\mathrm{get}\left(\mathrm{Square}.C\left(x\right),i\right)\right)\right)\ne \mathrm{Square}.\mathrm{target}\left(x\right)$$

Proof. Machine-checked in Lean as D5/S3/QuantumContext/RankOfContextualityNonPowerTwo.parity_miss (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. K. Horodecki; J. Zhou; M. Stankiewicz; R. Salazar; P. Horodecki; R. Raussendorf; R. Horodecki; R. Ramanathan; E. Tyhurst (2022). The rank of contextuality. DOI: 10.1088/1367-2630/acdf78. URL: https://arxiv.org/abs/2205.10307.

Commentary.

For every Boolean assignment to the nine observables, at least one of the six context parities differs from its prescribed target.

Lemma 1.13 (Context lookup agrees with square indexing).

$$\forall (s:Fin\left(6\right)),\forall (i:Fin\left(3\right)),\mathrm{List}.\mathrm{get}\left(\mathrm{Square}.C\left(s\right),i\right)=\mathrm{Square}.\mathrm{idx}\left(s,i\right)$$

Proof. Machine-checked in Lean as D5/S3/QuantumContext/RankOfContextualityNonPowerTwo.pm_get_idx (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. K. Horodecki; J. Zhou; M. Stankiewicz; R. Salazar; P. Horodecki; R. Raussendorf; R. Horodecki; R. Ramanathan; E. Tyhurst (2022). The rank of contextuality. DOI: 10.1088/1367-2630/acdf78. URL: https://arxiv.org/abs/2205.10307.

Commentary.

Looking up position i in the square context s gives its row-major observable index.

Theorem 1.14 (A quantum rank that is not a power of two).

$$claim$$

Proof. Machine-checked in Lean as D5/S3/QuantumContext/RankOfContextualityNonPowerTwo.result (✓ std3). ∎

Resolves. Problems/horodecki-2022-rank-of-contextuality-non-power-of-two (proved) by D5/S3/QuantumContext/RankOfContextualityNonPowerTwo.result.

Source. Repository-derived.

Acknowledgement. K. Horodecki; J. Zhou; M. Stankiewicz; R. Salazar; P. Horodecki; R. Raussendorf; R. Horodecki; R. Ramanathan; E. Tyhurst (2022). The rank of contextuality. DOI: 10.1088/1367-2630/acdf78. URL: https://arxiv.org/abs/2205.10307.

Commentary.

The behavior is the product of two Peres–Mermin squares: 18 observable labels, 36 paired contexts, and the maximally mixed state on Fin 16. Each square has five positive parity contexts and one negative parity context. For every context c, the uniform weight on the 16 assignments with the sole parity defect at c agrees with the square away from c. The three products with matching row defects cover every paired context, since at most two of the three rows occur in that pair. For the lower bound, each noncontextual product-scenario model has noncontextual copy marginals. One bad first-copy context for one model and one bad second-copy context for another produce a paired context that neither model reproduces. Thus every cover has at least three distinct members, and the displayed three-member cover is optimal. The rank is 3, which is odd and greater than one, so it is not 2^n for any natural n.

References

• Truth anchor: D5/S3/QuantumContext/RankOfContextualityNonPowerTwo.Behavior
• Truth anchor: D5/S3/QuantumContext/RankOfContextualityNonPowerTwo.IsQuantum
• Truth anchor: D5/S3/QuantumContext/RankOfContextualityNonPowerTwo.IsRankOfContextuality
• Truth anchor: D5/S3/QuantumContext/RankOfContextualityNonPowerTwo.NonContextual
• Truth anchor: D5/S3/QuantumContext/RankOfContextualityNonPowerTwo.bv_parity
• Truth anchor: D5/S3/QuantumContext/RankOfContextualityNonPowerTwo.claim
• Truth anchor: D5/S3/QuantumContext/RankOfContextualityNonPowerTwo.coverSizes
• Truth anchor: D5/S3/QuantumContext/RankOfContextualityNonPowerTwo.idx
• Truth anchor: D5/S3/QuantumContext/RankOfContextualityNonPowerTwo.parity3
• Truth anchor: D5/S3/QuantumContext/RankOfContextualityNonPowerTwo.parity_miss
• Truth anchor: D5/S3/QuantumContext/RankOfContextualityNonPowerTwo.pm_get_idx
• Truth anchor: D5/S3/QuantumContext/RankOfContextualityNonPowerTwo.restrict
• Truth anchor: D5/S3/QuantumContext/RankOfContextualityNonPowerTwo.result
• Truth anchor: D5/S3/QuantumContext/RankOfContextualityNonPowerTwo.target
• Dependency: D5/S3/Arith/FibonacciAtomic/NativeContinuation/JointLaw
• Dependency: D5/S3/Entropy/Forgetting/PushforwardComposition
• Dependency: D5/S3/Entropy/Observation/MultiTargetInformationChain
• Dependency: D5/S3/Quantum/FiniteDimensional
• Dependency: D5/S3/QuantumBounds/StatisticalStrengthMagicSquare