Condensation need not preserve LC-equivalence

Abstract

Two connected six-vertex graphs are related by local complementations and satisfy the bound of at most one outside neighbour for every vertex of the condensation set in both graphs, but their condensed graphs are not LC-equivalent. This refutes Conjecture 16 of Vandré, de Jong, Hahn, Burchardt, Gühne and Pappa.

Definition 1.1 (Condensed graph).

$$\forall V\in \mathrm{Type},\forall G\in \mathrm{SimpleGraph}\left(V\right),\forall C\in \mathrm{Finset}\left(V\right),\begin{array}{r}\mathrm{condense}\left(G,C\right):\mathrm{SimpleGraph}\left(\mathrm{Option}\left(\{v:V\mid \neg (v\in C)\}\right)\right)\\ \mathrm{Adj}\left(\mathrm{condense}\left(G,C\right),\mathrm{none},\mathrm{none}\right)\iff (\mathrm{False})\\ \forall i\in \{v:V\mid \neg (v\in C)\},\forall j\in \{v:V\mid \neg (v\in C)\},\mathrm{Adj}\left(\mathrm{condense}\left(G,C\right),\mathrm{some}\left(i\right),\mathrm{some}\left(j\right)\right)\iff (\mathrm{Adj}\left(G,\mathrm{val}\left(i\right),\mathrm{val}\left(j\right)\right))\\ \forall i\in \{v:V\mid \neg (v\in C)\},\mathrm{Adj}\left(\mathrm{condense}\left(G,C\right),\mathrm{some}\left(i\right),\mathrm{none}\right)\iff (\exists s\in V,(s\in C)\wedge (\mathrm{Adj}\left(G,\mathrm{val}\left(i\right),s\right)))\\ \forall i\in \{v:V\mid \neg (v\in C)\},\mathrm{Adj}\left(\mathrm{condense}\left(G,C\right),\mathrm{none},\mathrm{some}\left(i\right)\right)\iff (\exists s\in V,(s\in C)\wedge (\mathrm{Adj}\left(G,\mathrm{val}\left(i\right),s\right)))\end{array}$$

Formalization. D5/S3/Quantum/Entanglement/GraphCondensationLCRefutation.condense (✓ std3).

Citation. Lina Vandré; Jarn de Jong; Frederik Hahn; Adam Burchardt; Otfried Gühne; Anna Pappa (2024). Distinguishing Graph States by the Properties of Their Marginals. DOI: 10.48550/arXiv.2406.09956. URL: https://arxiv.org/abs/2406.09956v2.

Commentary.

Definition 13 (arXiv:2406.09956v2, p. 12): “Consider a graph G = (V, E) and a set C ⊆ V. The condensed graph G_C = (V_C, E_C) consists of the node set V_C = {c} ∪ (V \ C) and edge set E_C defined in the following way: (i, j) ∈ E_C if either i, j ∈ V \ C and (i, j) ∈ E, or j = c and there exists s ∈ C such that (i, s) ∈ E.” The fresh vertex c is none; an outside vertex is some(i), where i is a subtype element with val(i) ∉ C. The undirected adjacency is symmetrized, and none is not adjacent to itself. The graph type and the four adjacency cases below are the defining expression.

Definition 1.2 (Finite sequences of local complementations).

$$\forall V\in \mathrm{Type},\forall G\in \mathrm{SimpleGraph}\left(V\right),\forall H\in \mathrm{SimpleGraph}\left(V\right),\mathrm{LCEquivalent}\left(G,H\right)\iff (\exists s\in \mathrm{List}\left(V\right),H=\mathrm{lcSeq}\left(G,s\right))$$

Formalization. D5/S3/Quantum/Entanglement/GraphCondensationLCRefutation.LCEquivalent (✓ std3).

Citation. Lina Vandré; Jarn de Jong; Frederik Hahn; Adam Burchardt; Otfried Gühne; Anna Pappa (2024). Distinguishing Graph States by the Properties of Their Marginals. DOI: 10.48550/arXiv.2406.09956. URL: https://arxiv.org/abs/2406.09956v2.

Commentary.

LC-equivalence is existence of a finite list s of vertices such that H = lcSeq(G, s). Local complementation complements the edges between the selected vertex’s neighbours and preserves all other edges. The reused lcSeq applies these operations in list order. The paper states (p. 5): “There is a one-to-one correspondence between the local complementation orbit of a given graph and the orbit under local Clifford operations of the corresponding graph state.” Definition 4 (pp. 4–5) gives the local complementation formula; the correspondence cites Van den Nest, Dehaene and De Moor (2004).

Definition 1.3 (Conjecture 16).

$$claim\iff (\forall (V:\mathrm{Type})[\mathrm{Fintype}\left(V\right)][\mathrm{DecidableEq}\left(V\right)],\forall G\in \mathrm{SimpleGraph}\left(V\right),\forall H\in \mathrm{SimpleGraph}\left(V\right),\forall C\in \mathrm{Finset}\left(V\right),(\mathrm{Connected}\left(G\right))\Rightarrow ((\mathrm{Connected}\left(H\right))\Rightarrow ((\forall s\in V,(s\in C)\Rightarrow (\mathrm{card}\left(\mathrm{filter}\left(\mathrm{univ},i\mapsto ((\neg (i\in C))\wedge (\mathrm{Adj}\left(G,s,i\right)))\right)\right)\le 1))\Rightarrow ((\forall s\in V,(s\in C)\Rightarrow (\mathrm{card}\left(\mathrm{filter}\left(\mathrm{univ},i\mapsto ((\neg (i\in C))\wedge (\mathrm{Adj}\left(H,s,i\right)))\right)\right)\le 1))\Rightarrow ((\mathrm{LCEquivalent}\left(G,H\right))\Rightarrow (\mathrm{LCEquivalent}\left(\mathrm{condense}\left(G,C\right),\mathrm{condense}\left(H,C\right)\right)))))))$$

Formalization. D5/S3/Quantum/Entanglement/GraphCondensationLCRefutation.claim (✓ std3).

Citation. Lina Vandré; Jarn de Jong; Frederik Hahn; Adam Burchardt; Otfried Gühne; Anna Pappa (2024). Distinguishing Graph States by the Properties of Their Marginals. DOI: 10.48550/arXiv.2406.09956. URL: https://arxiv.org/abs/2406.09956v2.

Commentary.

Conjecture 16 (arXiv:2406.09956v2, p. 13): “Given two graphs G and G′ and a condensation set C such that each node in C is connected to at most one node in the neighborhood in V \ C. If G and G′ are LC-equivalent, it follows that G_c and G′_c are LC-equivalent.” V is any finite labelled vertex type with decidable equality, G and H encode G and G′, and C is a finset. The bracketed [Fintype V] and [DecidableEq V] terms are the anonymous Lean typeclass assumptions. Both graphs are connected, as the paper assumes for its simple graphs. The outside-neighbour bound is required in both graphs: the cardinality of {i in V | i ∉ C and Adj(G, s, i)} is at most one for every s ∈ C, and likewise for H. The function filter selects precisely these vertices from univ; card is finset cardinality. This reading meets the degree condition on both sides.

Theorem 1.4 (Six vertices refute the conjecture).

$$\neg claim$$

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

Resolves. Problems/vandre-2024-graph-condensation-lc-equivalence-refutation (refuted) by D5/S3/Quantum/Entanglement/GraphCondensationLCRefutation.result.

Source. Repository-derived.

Acknowledgement. Lina Vandré; Jarn de Jong; Frederik Hahn; Adam Burchardt; Otfried Gühne; Anna Pappa (2024). Distinguishing Graph States by the Properties of Their Marginals. DOI: 10.48550/arXiv.2406.09956. URL: https://arxiv.org/abs/2406.09956v2.

Commentary.

On Fin(6), take C = {0, 1, 2}, E(G) = {01, 02, 05, 14, 23} and E(H) = {05, 14, 23, 35, 45}. Both graphs are connected and each vertex of C has exactly one outside neighbour. Complementing at 0, 1, 2, 3, 4, 5 in order maps G to H. Condensation gives Mathlib’s star graph with centre none and leaves 3, 4, 5, and the diamond with edges {c3, c4, c5, 35, 45}. The family consisting of the complete graph and every star is closed under local complementation: at a star’s centre it gives the complete graph, at a leaf it preserves the star, and at a vertex of the complete graph it gives the star centred there. Induction over the list of operations keeps the condensed first graph in this family. The diamond is neither complete nor any of the four stars, as specific adjacency comparisons show, so it cannot be reached. On four vertices the family’s graphs have three or six edges, while the diamond has five.

References

• Truth anchor: D5/S3/Quantum/Entanglement/GraphCondensationLCRefutation.LCEquivalent
• Truth anchor: D5/S3/Quantum/Entanglement/GraphCondensationLCRefutation.claim
• Truth anchor: D5/S3/Quantum/Entanglement/GraphCondensationLCRefutation.condense
• Truth anchor: D5/S3/Quantum/Entanglement/GraphCondensationLCRefutation.result
• Dependency: D5/S3/Quantum/Entanglement/GraphStateMonogamyForbiddenSubgraph