Metadata
slug: wu-2014-randomized-graph-negativity-monotonicity
bibkey: wu2014randomized
doi: 10.1103/PhysRevA.89.052335
url: https://arxiv.org/abs/1403.3828v3
triage: theorem
motivation_gids:
- D5/S3/Quantum/Entanglement/RandomizedGraphNegativityRefutation.result
Monotonicity of the negativity of randomized graph states
Problem
J.-Y. Wu, M. Rossi, H. Kampermann, S. Severini, L. C. Kwek, C. Macchiavello, D. Bruß, Randomized Graph States and their Entanglement Properties, Phys. Rev. A 89, 052335 (2014), arXiv:1403.3828v3, Section V:
However, even though this conjecture is supported by numerical evidence, it is an open question whether the monotonic behavior of the negativity in terms of the randomness is a common feature to all RG states.
The randomized graph state of a graph is $\rho^p_G=\sum_{F\subseteq E(G)}p^{|F|}(1-p)^{|E(G)\setminus F|} |F\rangle\langle F||F\rangle=\prod_{ab\in F}\mathrm{CZ}_{ab} |+\rangle^{\otimes n}A|B$ is , evaluated “with respect to all possible bipartitions of the qubits”. The conjecture is that increases monotonically in ; the paper reports it numerically for the complete graphs and the star graphs with .
Motivation
A randomized graph state models the preparation of a graph state with
probabilistic entangling gates: every controlled-Z gate succeeds with
probability and the record of which gates succeeded is lost. At
the state is the product state and at it is
the graph state of , so one expects more entanglement for more reliable
gates. The question asks whether this holds for every graph and every cut.
The frozen declaration
D5/S3/Quantum/Entanglement/RandomizedGraphNegativityRefutation.result
answers it negatively.
Gap
Issue #12382 classifies the question as Tier 1 and records the checks made before any Lean:
- arXiv:1403.3828 v3 (2014-06-03) is the latest version and the published version, and the question is printed as quoted;
- Salem–Silva–Andrade, arXiv:2310.20418v2 (Phys. Rev. A 109, 012416, 2024), Sec. IV, report non-monotonic entanglement only for randomized hypergraph states with hyperedges of different orders and write that “such behavior could not be observed in RG states”; their arXiv:2506.20075v2 (2026), Fig. 3 caption, states “Monotonicity holds for hypergraphs with uniform hyperedge orders”; the review Poderini–Bruß–Macchiavello, arXiv:2603.10917v1 (2026), Sec. III.4, attributes non-monotonicity to non-uniform hypergraphs;
- noisy and percolated graph-state results (Aolita et al., arXiv:1006.3152; Kieling–Rudolph–Eisert, quant-ph/0611140) concern other models.
These are orchestrator-reported and seat-reported readings,
not-found-in-searched-scope; they do not establish exhaustive worldwide
novelty. Convexity of the trace norm bounds the negativity of the mixture
from above by the average negativity of the graph states , so
the large negativity of some subgraph states does not by itself give a
lower bound for the mixture.
Route
on with parts and , and .
- Expanding the product over the edges, with if and otherwise; so the partial transpose has entries , where counts the edges on which the exchanged labels disagree.
- At , with , and , the entrywise identity $X_1+\tfrac1{128}ww^{\mathsf T}=\tfrac1{64}(u_{00}u_{00}^{\mathsf T} +u_{11}u_{11}^{\mathsf T})+\tfrac1{128}vv^{\mathsf T}X_1$ as a difference of two positive semidefinite matrices with traces and ; the triangle inequality gives , so .
- At , fourteen pairwise orthogonal integer vectors give the projection and the unitary ; by the variational formula , $|X_{97/100}|1\ge1-2\sum_ju_j^{\mathsf T}X{97/100}u_j/|u_j|^2 =2.0280536\ldots>2$.
- Hence with .
Falsifier
The kernel-checked result is the negation of the universal statement
over finite simple graphs on Fin n, subsets of the vertices and all
real . The basis states are the maps Fin n → Bool, the
graph state of an edge set is its product of controlled-Z phases times the
amplitude of , the mixture runs over the
subsets of G.edgeFinset, the partial transposition is the frozen
CycleFiveStrongOneResistance.transposePart (it exchanges the parts of
the row and column labels), and the trace norm is the frozen
FiniteTraceDistance.traceNorm, $\operatorname{Re}\operatorname{Tr}
\sqrt{X^\dagger X}N$, such
as the logarithmic negativity , is refuted as well;
restricting the question to and changes the question.
Evidence
Exhaustive NumPy scan of the connected graphs on 4–6 vertices, all bipartitions and (issue #12382): five pairs , all on 6 vertices, show a decrease; none on 4 or 5 vertices. The largest is this example: rises above on with maximum near , and the derivative at is about (finite difference). The exact lower bound of step 3 is . The certificate vectors split by the symmetry of the parts (six in the symmetric sector, two in each mixed sector, four in the standard–standard sector).
The canonical source is
D5/S3/Quantum/Entanglement/RandomizedGraphNegativityRefutation.lean. Its
public declarations are Qubits, czPhase, plusState, graphState,
rgState, negativity, claim, k33, partA and result; the
partial transposition is the frozen
D5/S3/Quantum/Entanglement/CycleFiveStrongOneResistance.transposePart, and
the trace norm and its lemmas are frozen in
D5/S3/Quantum/Foundation/FiniteTraceDistance; k33 carries a decidable
adjacency instance. The frozen module state has statement identity
sha256:a40b0f5478e2394807b3cd5c3fe6678251f25ad3e25d09ddd424e32bc01e1f60. The
result declaration has statement identity
sha256:8699682eb0805d4dcf1355be31c5dac754e3a40e309a3d295ac441cf8ab56906. The
Freeze event is
sha256:cb386a648738573ec8ccc5fa15cead0984628eb4c316f21e726fda95f4cae172; its
project-level frozen prerequisites are the Freeze events of
D5/S3/Quantum/Foundation/FiniteTraceDistance and
D5/S3/Quantum/Entanglement/CycleFiveStrongOneResistance. The proof uses only the standard axioms propext, Classical.choice and
Quot.sound; no sorry, native_decide, or new axiom.
Triage
Tier 1 published question; resolution Refuted by
D5/S3/Quantum/Entanglement/RandomizedGraphNegativityRefutation.result.
proof_shape: content; admission_basis: open-problem-resolution (issue
#12382). Utility kind certified-instance, basis refutes the module’s
claim.
What the settlement shows
- Proved by
result: the negativity of randomized graph states is not monotone in : for across its two parts it is larger at than at . - Proved inside the proof of
result: the closed form of the partial transpose for at every ; the decomposition of step 2, giving ; and the bound from the explicit unitary . - Mechanism (computed, not stated in Lean): a graph state across a cut has negativity , where is the rank over GF(2) of the biadjacency matrix of the cut (checked by singular values for all spanning subgraphs of ). The biadjacency matrix of is the all-ones matrix, , so the endpoint has ; deleting any one edge raises to (), and among the spanning subgraphs have . Near the mixture puts weight about on the one-edge deletions, and the computed negativity grows. In the scan, all five decreasing pairs have for the full graph and a single-edge deletion with ; among the pairs where no single-edge deletion raises , none decreases, and of the pairs where one does are still monotone on the grid.
- Computed, not in Lean: also decreases slightly on (from to ); with the part of size decreases by between and while its maximum is at .
- Follows from it (not stated in Lean): the statements of Salem–Silva–Andrade that non-monotonic behaviour “could not be observed in RG states” (2024) and that monotonicity holds for hypergraphs with uniform hyperedge orders (2026) do not extend to all ordinary graphs, since is 2-uniform; by continuity the decrease also holds against some .
- Open here: a characterization of the pairs with monotone negativity (the rank condition above is necessary on the scanned graphs but not sufficient, and its necessity in general is not proved); whether the complete graphs and the stars , the families of the paper’s numerics, are monotone for all ; and the sign of at , which the first-order perturbation of the trace norm ties to the kernel of .
ASSUMED-UNVERIFIED
Mansour et al., Laser Phys. 31, 035201 (2021), “Decay of negativity of randomized multiqubit mixed states”, was not read in full; Salem–Silva– Andrade (2024, ref. [40]) describe it as observing monotonic negativity for states generated by random Ising-type entangling operators. The literature checks do not establish worldwide priority. The Lean kernel verifies the encoded statement and its axiom closure; its correspondence to the paper, including the reading of the question as a universal statement over all graphs, bipartitions and pairs , is checked by reading the source and the definitions.