pith. sign in

arxiv: 2501.17556 · v4 · submitted 2025-01-29 · 💻 cs.LO

Trees in graphs of large linear cliquewidth

Miko{\l}aj Boja\'nczyk , Pierre Ohlmann This is my paper

Pith reviewed 2026-05-23 05:18 UTC · model grok-4.3

classification 💻 cs.LO
keywords cliquewidthlinear cliquewidthMSO transductionsinduced subgraphstreesgraph classestransduction orderpathwidth theorem
0
0 comments X

The pith

Every graph class with bounded cliquewidth but unbounded linear cliquewidth contains arbitrarily large tree-like patterns as induced subgraphs that MSO-transduce all trees.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes an analogue of the Pathwidth Theorem for classes of dense graphs. If a class has bounded cliquewidth yet unbounded linear cliquewidth, it must contain larger and larger copies of certain specific tree-like patterns appearing as induced subgraphs. These patterns can be used with monadic second-order logic to define or generate every possible tree. The result also shows that subdivisions of binary trees can be obtained using first-order logic from the same patterns. This supplies the final step needed to prove that the CMSO transduction ordering on graph classes is total, so that any two classes can be compared in terms of their logical power.

Core claim

We give a finite family of tree-like patterns and prove that every graph class of bounded cliquewidth and unbounded linear cliquewidth contains arbitrarily large patterns as induced subgraphs. These patterns MSO transduce all trees, and FO transduce subdivisions of all binary trees. In particular, our result provides the missing piece in establishing that the CMSO transduction order is total over classes of finite graphs.

What carries the argument

A finite family of tree-like patterns that occur as induced subgraphs and support MSO transductions of arbitrary trees.

Load-bearing premise

A finite family of tree-like patterns exists such that their induced occurrences in any bounded-cliquewidth unbounded-linear-cliquewidth class are enough to MSO-transduce every tree.

What would settle it

Construct or exhibit a specific graph class that has bounded cliquewidth, unbounded linear cliquewidth, yet avoids arbitrarily large copies of all the tree-like patterns in the family.

Figures

Figures reproduced from arXiv: 2501.17556 by Miko{\l}aj Boja\'nczyk, Pierre Ohlmann.

Figure 1
Figure 1. Figure 1: Inner and outer suffixes and prefixes. are linear. Now we observe that if we take a node X of the new tree decomposition, then the factor of X in the original tree decomposition describes the part between X and its children in the new tree decomposition. Therefore, the sibling sub-decompositions of the new tree decompositions are linear. Applying the induction basis we then get that the new decomposition i… view at source ↗
Figure 2
Figure 2. Figure 2: The paths P1 and P2. Proof. We proceed in the same way as in Claim A.61. Suppose that A B and C D satisfy the assumptions of Claim A.63. Apply the claim, yielding condition (*). Using Lemma A.10, choose some recolouring e such that Te = {T ∣ T is a sub-decomposition of T where all contexts have recolouring e } has unbounded Strahler number. We will use the Covering Lemma for the obstruction from Claim A.64… view at source ↗
read the original abstract

The Pathwidth Theorem states that if a class of graphs has unbounded pathwidth, then it contains all trees as graph minors. We prove a similar result for dense graphs. More precisely, we give a finite family of tree-like patterns and prove that every graph class of bounded cliquewidth and unbounded linear cliquewidth contains arbitrarily large patterns as induced subgraphs. These patterns mso transduce all trees, and fo transduce subdivisions of all binary trees. In particular, our result provides the missing piece in establishing that the cmso transduction order is total over classes of finite graphs.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The paper establishes an analogue of the Pathwidth Theorem for dense graphs: every class of graphs with bounded cliquewidth but unbounded linear cliquewidth contains arbitrarily large induced copies of a finite family of tree-like patterns. These patterns admit MSO-transductions to all trees and FO-transductions to subdivisions of all binary trees. The result supplies the missing piece needed to conclude that the CMSO transduction order is total over all classes of finite graphs, via an explicit construction of the pattern family (by case analysis on linear-cliquewidth decompositions) and a reduction of the unavoidability statement to the Pathwidth Theorem through a dense analogue.

Significance. The result completes a major structural theorem on the totality of the CMSO transduction order, which has implications for the logical and algorithmic study of graph classes. The explicit finite family constructed in §3, together with the verified transduction definitions and the reduction to a prior theorem, provides a self-contained and falsifiable contribution. The work strengthens the existing theory by handling the bounded-cliquewidth/unbounded-linear-cliquewidth regime uniformly.

minor comments (3)
  1. §3: the case analysis on linear-cliquewidth decompositions is described as exhaustive, but a brief remark on why the number of cases remains finite (independent of the particular decomposition width) would aid readability.
  2. The transduction definitions in §4 could include a short diagram or pseudocode sketch of how an occurrence of a pattern is mapped to a tree, to make the MSO/FO formulas easier to verify at a glance.
  3. Notation: the paper uses both 'linear cliquewidth' and 'lcw' without an explicit first-use definition; adding a parenthetical on first occurrence would prevent minor confusion for readers outside the immediate subfield.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary, significance assessment, and recommendation to accept the manuscript.

Circularity Check

0 steps flagged

No significant circularity; derivation self-contained

full rationale

The paper explicitly constructs a finite family of tree-like patterns via case analysis on linear cliquewidth decompositions (§3) and defines the MSO/FO transductions mapping them to trees and binary-tree subdivisions. The unavoidability claim reduces to the external Pathwidth Theorem via a dense analogue, with no equations, fitted parameters, or self-citations that bear the central load. No step reduces by construction to the paper's own inputs; the argument is independent of any prior fitted values or author-overlapping uniqueness theorems.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The claim rests on standard definitions of cliquewidth, linear cliquewidth, MSO and FO transductions, and the Pathwidth Theorem; no free parameters, new entities, or ad-hoc axioms are introduced in the abstract.

axioms (2)
  • standard math Standard definitions of cliquewidth, linear cliquewidth, MSO logic, FO logic, and graph transductions from the literature.
    The result is stated using these established notions; the abstract invokes them without re-deriving them.
  • standard math The Pathwidth Theorem (unbounded pathwidth implies all trees as minors).
    The paper explicitly positions its result as an analogue of this known theorem.

pith-pipeline@v0.9.0 · 5622 in / 1531 out tokens · 53062 ms · 2026-05-23T05:18:33.458184+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

84 extracted references · 84 canonical work pages

  1. [1]

    Problems easy for tree-decomposable graphs extended abstract

    Stefan Arnborg, Jens Lagergren, and Detlef Seese. Problems easy for tree-decomposable graphs extended abstract. In Timo Lepist ¨o and Arto Salomaa, editors,Automata, Languages and Programming, pages 38–51, Berlin, Heidelberg, 1988. Springer Berlin Heidelberg

    work page 1988

  2. [2]

    On the Monadic Second- Order Transduction Hierarchy.Logical Methods in Computer Science, Volume 6, Issue 2, June 2010

    Achim Blumensath and Bruno Courcelle. On the Monadic Second- Order Transduction Hierarchy.Logical Methods in Computer Science, Volume 6, Issue 2, June 2010. 12

    work page 2010

  3. [3]

    Bodlaender

    Hans L. Bodlaender. A linear time algorithm for finding tree- decompositions of small treewidth. InProceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing, STOC ’93, pages 226– 234, New York, NY, USA, 1993. Association for Computing Machinery

    work page 1993

  4. [4]

    The category of MSO transductions.CoRR, abs/2305.18039, 2023

    Mikolaj Bojanczyk. The category of MSO transductions.CoRR, abs/2305.18039, 2023

    work page arXiv 2023

  5. [5]

    Folding interpretations

    Mikołaj Boja ´nczyk. Folding interpretations. InLogic in Computer Science, LICS ’22. Association for Computing Machinery, 2023

    work page 2023

  6. [6]

    Definable decompositions for graphs of bounded linear cliquewidth.Logical Methods in Computer Science, Volume 17, Issue 1, January 2021

    Mikołaj Boja ´nczyk, Martin Grohe, and Michał Pilipczuk. Definable decompositions for graphs of bounded linear cliquewidth.Logical Methods in Computer Science, Volume 17, Issue 1, January 2021

    work page 2021

  7. [7]

    Rank-decreasing transduc- tions

    Mikolaj Boja ´nczyk and Pierre Ohlmann. Rank-decreasing transduc- tions. InLICS, 2024

    work page 2024

  8. [8]

    Definability equals recog- nizability for graphs of bounded treewidth

    Mikołaj Boja ´nczyk and Michal Pilipczuk. Definability equals recog- nizability for graphs of bounded treewidth. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors,Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016, pages 407–416. ACM, 2016

    work page 2016

  9. [9]

    A Combinatorial Theorem for Trees

    Thomas Colcombet. A Combinatorial Theorem for Trees. InInterna- tional Colloquium on Automata, Languages and Programming, ICALP, Wrocław, Poland, Lecture Notes in Computer Science, pages 901–912. Springer, 2007

    work page 2007

  10. [10]

    The monadic second-order logic of graphs

    Bruno Courcelle. The monadic second-order logic of graphs. I. Recog- nizable sets of finite graphs.Information and Computation, 85(1):12–75, March 1990

    work page 1990

  11. [11]

    The monadic second-order logic of graphs v: on closing the gap between definability and recognizability.Theoretical Computer Science, 80(2):153 – 202, 1991

    Bruno Courcelle. The monadic second-order logic of graphs v: on closing the gap between definability and recognizability.Theoretical Computer Science, 80(2):153 – 202, 1991

    work page 1991

  12. [12]

    A logical characterisation of the sets of hypergraphs defined by hyperedge replacement grammars

    Bruno Courcelle and Joost Engelfriet. A logical characterisation of the sets of hypergraphs defined by hyperedge replacement grammars. Mathematical Systems Theory, 28(6):515–552, 1995

    work page 1995

  13. [13]

    Cambridge University Press, 2012

    Bruno Courcelle and Joost Engelfriet.Graph Structure and Monadic Second-Order Logic - A Language-Theoretic Approach, volume 138 of Encyclopedia of Mathematics and Its Applications. Cambridge University Press, 2012

    work page 2012

  14. [14]

    Vertex-minors, monadic second- order logic, and a conjecture by seese.Journal of Combinatorial Theory, Series B, 97(1):91–126, 2007

    Bruno Courcelle and Sang-il Oum. Vertex-minors, monadic second- order logic, and a conjecture by seese.Journal of Combinatorial Theory, Series B, 97(1):91–126, 2007

    work page 2007

  15. [15]

    A characterization of context-free nce graph languages by monadic second-order logic on trees

    Joost Engelfriet. A characterization of context-free nce graph languages by monadic second-order logic on trees. In Hartmut Ehrig, Hans-J ¨org Kreowski, and Grzegorz Rozenberg, editors,Graph Grammars and Their Application to Computer Science, pages 311–327, Berlin, Heidelberg,

    work page

  16. [16]

    Springer Berlin Heidelberg

    work page

  17. [17]

    Stable graphs of bounded twin-width.CoRR, abs/2107.03711, 2021

    Jakub Gajarsk ´y, Michal Pilipczuk, and Szymon Torunczyk. Stable graphs of bounded twin-width.CoRR, abs/2107.03711, 2021

    work page arXiv 2021

  18. [18]

    Excluding a planar graph from gf (q)-representable matroids.Journal of Combinatorial Theory, Series B, 97(6):971–998, 2007

    Jim Geelen, Bert Gerards, and Geoff Whittle. Excluding a planar graph from gf (q)-representable matroids.Journal of Combinatorial Theory, Series B, 97(6):971–998, 2007

    work page 2007

  19. [19]

    Linear rank-width of distance-hereditary graphs ii

    Mamadou Moustapha Kant ´e and O-joung Kwon. Linear rank-width of distance-hereditary graphs ii. vertex-minor obstructions.European Journal of Combinatorics, 74:110–139, 2018

    work page 2018

  20. [20]

    Vertex-minors of graphs: A survey

    Donggyu Kim and Sang-il Oum. Vertex-minors of graphs: A survey. Discrete Applied Mathematics, 351:54–73, 2024

    work page 2024

  21. [21]

    Springer, 2004

    Leonid Libkin.Elements of finite model theory, volume 41. Springer, 2004

    work page 2004

  22. [22]

    Regularity lemmas for fixpoint graphs.Transactions of the American Mathematical Society, 366(3):1551–1585, 2014

    Maryanthe Malliaris and Saharon Shelah. Regularity lemmas for fixpoint graphs.Transactions of the American Mathematical Society, 366(3):1551–1585, 2014

    work page 2014

  23. [23]

    Sang-il Oum and Paul D. Seymour. Approximating clique-width and branch-width.J. Comb. Theory B, 96(4):514–528, 2006

    work page 2006

  24. [24]

    Neil Robertson and Paul D. Seymour. Graph minors. i. excluding a forest.J. Comb. Theory B, 35(1):39–61, 1983

    work page 1983

  25. [25]

    Graph minors

    Neil Robertson and Paul D Seymour. Graph minors. v. excluding a planar graph.Journal of Combinatorial Theory, Series B, 41(1):92–114, 1986

    work page 1986

  26. [26]

    The structure of the models of decidable monadic theories of graphs.Annals of pure and applied logic, 53(2):169–195, 1991

    Detlef Seese. The structure of the models of decidable monadic theories of graphs.Annals of pure and applied logic, 53(2):169–195, 1991

    work page 1991

  27. [27]

    The Monadic Theory of Order.Annals of Mathematics, pages 379–419, 1975

    Saharon Shelah. The Monadic Theory of Order.Annals of Mathematics, pages 379–419, 1975

    work page 1975

  28. [28]

    Factorisation forests of finite height.Theoretical Computer Science, 72(1):65–94, 1990

    Imre Simon. Factorisation forests of finite height.Theoretical Computer Science, 72(1):65–94, 1990

    work page 1990

  29. [29]

    Factorisation forests of finite height.Theoret

    Imre Simon. Factorisation forests of finite height.Theoret. Comput. Sci., 72(1):65–94, 1990. Appendix Appendix to Section II In this part of the appendix, add some clarifications, extra material, and missing proofs for the results from the prelim- inaries. A. Terms and regular classes of graphs In this part of the appendix, we describe regular classes of ...

    work page 1990

  30. [30]

    aninitial graphwithkcolours; and

    work page

  31. [31]

    abinary graph termof typek×k→k. The class of graphsgeneratedby a template is the least class ofk-coloured graphs that contains the initial graph, and which is closed under applying the (operation corresponding to the) binary graph term. A class of graphs is calledregularif it is generated by one template. Many interesting phenomena can be observed already...

    work page

  32. [32]

    there is a tree minor which has Strahler number at least n, and such that every disjoint pair of nodes in this minor belongs to the Strahler constraint; or

    work page

  33. [33]

    Proof.A simple extraction argument

    there is a split of heightnsuch that on every layer, there is no disjoint pair from the Strahler constraint. Proof.A simple extraction argument. Define a split as fol- lows: to each nodeXwe associate the largestnsuch that the subtree ofTrooted atXsatisfies the first item, with the inherited Strahler constraint. Consider a layerSof this split, and a pair o...

    work page

  34. [34]

    the heights of the splits are bounded

    work page

  35. [35]

    the local sub-decompositions have linearisations of bounded width

    work page

  36. [36]

    ThenTalso has linearisations of bounded width

    the layer sub-decompositions of the splits have linearisa- tions of bounded width. ThenTalso has linearisations of bounded width. Proof.Fix a classTas in the assumption of the lemma. For every tree decomposition from this class, when talking about the split, we mean the associated split from the assumption of the lemma. Define aninternal nodein a tree to ...

    work page

  37. [37]

    for each part of the outer preorder, aninner preorder. Then the width of the corresponding combined preorder is at most: 2 width of inner preorder+3⋅(width of outer preorder) Proof of the claim.Recall the comments in Footnote 3 about the alternative notions of rank. In this proof, it will be more convenient to work with the matrix rank, in the two element...

    work page

  38. [38]

    For the layer sub-decompositions, we simply use as- sumption 3 for the original tree decomposition

    work page

  39. [39]

    aandbare mapped to the same colour

    We now prove that the local sub-decompositions of the new tree decomposition are linear. For a nodeXin the original tree decompositionT, define itsfactorto be the following set of nodes: {Y∣ Yis a (not necessarily proper) descendant ofXinTand all nodes strictly between XandYhave non-maximal level }. The idea is that we start inX, and we keep on going down...

    work page

  40. [40]

    its profile is a partial function; and

    work page

  41. [41]

    this partial function is idempotent

    work page

  42. [42]

    Proof.We begin with the first item, about partial functions

    if an outer componentAis such that(A, A)belongs to the profile of some context in the tree decomposition, then it belongs to the profiles of all contexts. Proof.We begin with the first item, about partial functions. Claim A.20.For every context and every outer component A, there is at most one outer componentBsuch that(A, B) belongs to the profile of the ...

    work page

  43. [43]

    only local edges; and

    work page

  44. [44]

    one recurrent outer component; and

    work page

  45. [45]

    Then there isk∈{0,1,2,

    unbounded Strahler number. Then there isk∈{0,1,2, . . .}such that every acyclic graph can be obtained from some graph (underlying a tree decomposition) inTby applying some a sequence of vertex deletions and≤k independent contractions. Proof of Lemma A.28.LetAbe the unique outer component that is recurrent, from the second assumption in the lemma. Recall f...

    work page

  46. [46]

    the subgraph induced by the center is connected

    work page

  47. [47]

    Proof.LetGbe the unary graph term that is induced by the context

    every path fromXto a vertex outsideYmust use a vertex from the center. Proof.LetGbe the unary graph term that is induced by the context. Note that the property in the statement of the claim can be expressed inmsowith quantifier rank at most 2: this is because being connected to a vertex outside of Yis a property of the colours withinY; we say that a colou...

    work page

  48. [48]

    has the local edge property

    work page

  49. [49]

    there are at least two outer components that are recurrent

    work page

  50. [50]

    Proof.The proof will be based on an extended analysis of connectivity

    the local sub-decompositions have linearisations of bounded width; ThenThas linearisations of bounded width. Proof.The proof will be based on an extended analysis of connectivity. The following claim shows that a colour from an outer component can only be used in the node that introduces a vertex. 24 Claim A.34.LetAbe an outer component, recurrent or not....

    work page

  51. [51]

    We are now ready to state the key technical result in this section

    there is a path fromX.AtoZ.A(this is becauseA↦A belongs to the profile ofZ⊂X). We are now ready to state the key technical result in this section. Claim A.37.LetAandBbe different recurrent components, and letYbe a node. Then every path in the induced subgraph ofYfromY.AtoY.Bmust pass through all descendants of Yin the tree decomposition. Proof.LetXbe a de...

    work page

  52. [52]

    This is because thanks to Claim A.37, there are no edges between two different red parts

    It cannot be the case that bothvandware in red parts. This is because thanks to Claim A.37, there are no edges between two different red parts

    work page

  53. [53]

    LetX i be the child that containsv

    Suppose now that the earlier vertexvbelongs to a black part, and the later vertexwbelongs to a red part. LetX i be the child that containsv. Using the edge to the later vertexw, we get a path fromvtoX.B, which does not visit nodeX i except for the first vertex. This is an outer path fromX i toX.B. The source of such a path must belong to eitherX i.AorX i....

    work page

  54. [54]

    A symmetric argument works when the earlier vertex is red and the later vertex is black

    work page

  55. [55]

    both belong to childrenX i andX j, withi<j

    Suppose now that both vertices are black, i.e. both belong to childrenX i andX j, withi<j. By Claim A.37, these children are consecutive, i.e.j=i+1. By the same reasoning as in the previous cases, we know that the earlier vertex belongs to the last part ofX i, and the later vertex belongs to the first part ofX j. These parts are at distance one or two in ...

    work page

  56. [56]

    for some fixpoint coloura∈Aand some contextX⊂Y in the class, there is an edge from portato some vertex with supercolourBinY∖X

    work page

  57. [57]

    being a context whereais good

    for every fixpoint coloura∈Aand every contextX⊂Y in the class, there is an edge portato some vertex with supercolourBinY∖X. Proof.The proof follows the same lines as the proof of Lemma A.16 Let us say that fixpoint coloura∈Aisgood in a contextX⊂Yif it has an edge to some vertex with supercolourBinY∖X. In this terminology, we want to show that if some fixp...

    work page

  58. [58]

    entanglement in some direction:A/⊙⊗⊚◻⧅◇⊗⧅◽d◾⊡BorB/⊙⊗⊚◻⧅◇⊗⧅◽d◾⊡A; or

    work page

  59. [59]

    for every two vertices with supercoloursAandB, respec- tively, that are introduced in non-nearby nodes, they are not connected by an edge; or

    work page

  60. [60]

    Proof.We say that there is ayes-connectionfrom supercolour Ato supercolourBif condition 1 from Lemma A.43 are satisfied

    for every two vertices with supercoloursAandB, respec- tively, that are introduced in non-nearby nodes, they are connected by an edge. Proof.We say that there is ayes-connectionfrom supercolour Ato supercolourBif condition 1 from Lemma A.43 are satisfied. We say that there is ano-connectionfromAtoB if there is a yes-connection after complementing the edge...

    work page

  61. [61]

    for every template that arises from the obstruction by choosing some initial graph, the class of graphs generated by the template transduces all trees

    work page

  62. [62]

    piece” of the tree decomposition, one of the binary terms from the set is ‘covered

    for both arguments in the obstruction, the corresponding recolouring is the identity. In the definition of obstructions, the trees (i.e. acyclic graphs) are transduced usingmso. In fact, in all obstructions that we consider in this paper, the trees will be transduced using first-order logic. Let us give some examples of obstruc- tions. Example 10.Consider...

    work page

  63. [63]

    ThenTtransduces all trees

    every tree decomposition inTcoversO. ThenTtransduces all trees. Proof.We begin by showing that, without loss of generality, assumption 2 can be strengthened to saying that every bicontext, not necessarily separated, covers some obstruction fromO. This is done by taking appropriate tree minors. Define aseparated minorof a treeTto be a tree minorS≤T which i...

    work page

  64. [64]

    an obstruction fromO

    work page

  65. [65]

    A profile isrealizedby a bicontext if the obstruction from the first item is covered using the superflips from the second item

    a set of superflips. A profile isrealizedby a bicontext if the obstruction from the first item is covered using the superflips from the second item. More formally, the obstruction is obtained applying the superflips from the second item (in whichever order), and then doing a sequence of local contractions and vertex deletions. We know that every bicontext...

    work page

  66. [66]

    for some profileσ, the classThas minors of unbounded Strahler number where every two disjoint nodes belongs to the side constraint corresponding toσ; or

    work page

  67. [67]

    is not an edge

    one can associate to each tree decomposition fromTa split, such that the splits have bounded height, and on each layer of the split, no pair of nodes belongs to any of the side constraints. The second option is impossible, because every bicontext has some profile. Therefore, the first option must hold. To complete the proof of the claim, we observe that i...

    work page

  68. [68]

    for every orientation, they are oriented in the same direc- tion; or

    work page

  69. [69]

    The following claim shows that consistent orientations are an equivalent way of defining bipolar orientations

    for every orientation, they are oriented in opposite direc- tions. The following claim shows that consistent orientations are an equivalent way of defining bipolar orientations. Claim A.57.The classTis polarized if and only if every two entangled pairs are oriented consistently. Proof.For the right-to-left implication, we observe that if all pairs are ori...

    work page

  70. [70]

    Leta, b, cbe the images ofA, B, Cunder the recolouringe

    Suppose thatA/⊙⊗⊚◻⧅◇⊗⧅◽d◾⊡BandB/⊙⊗⊚◻⧅◇⊗⧅◽d◾⊡Care oriented in the same direction by→. Leta, b, cbe the images ofA, B, Cunder the recolouringe. Here is a picture of the situation: The dotted lines in the picture mean that there may or may not be an edge. By flipping the supercoloursAand C, we know that either there is no edge betweenaandc, or there is one e...

    work page

  71. [71]

    Suppose now thatA/⊙⊗⊚◻⧅◇⊗⧅◽d◾⊡BandB/⊙⊗⊚◻⧅◇⊗⧅◽d◾⊡Care oriented in opposite directions by→. Using a similar argument as in the previous case, we see that the bicontextX 1, X2 ⊆X contains the following as an induced subgraph: After flipping the supercoloursBC, we get an obstruc- tion fromO. So far, we have proved that overlapping entangled pairs must be orie...

    work page

  72. [72]

    they are not oriented consistently

    work page

  73. [73]

    every” can be replaced by “some

    there is a path fromBtoCthat uses only local colours internally. Then every contextX⊂Yand every recolouringehas the following property: (*) If we definea, b, c, dto be the images ofA, B, C, D undere, then one can find pathsP 1 andP 2 which use only vertices introduced by the context, and satisfy the conditions explained in Figure 2. Proof.By Claim A.62, w...

    work page

  74. [74]

    for some orientation→and recolouringe, some context which has a cut that is consistent→ande

    work page

  75. [75]

    Proof.Before continuing with the proof, let us draw attention to a certain distinction

    for every orientation→and recolouringe, every context has a cut that is consistent with→ande. Proof.Before continuing with the proof, let us draw attention to a certain distinction. For each context, we associate two similar sets of vertices: Y∖X⌟⟨⟨⟪rl⟫l⟩⟩⟪⌟⟪⟨⟨⟪rl⟫mo⟨⌟⟪⟨⟨⟪rl⟫mo⟨⌟⟪⟨⟨⟪rl⟫mo⟨⌟⟪⟨⟨⟪rl⟫mo⟨⌟⟪⟨⟨⟪rl⟫mo⟨⌟⟪⟨⟨⟪rl⟫mo⟨⌟⟨⟨⟪rl⟫m⟩⟨⌟⟪⟨⟨⟪rl⟫mo⟨⌟⟪⟨⟨⟪rl⟫mo⟨⌟⟪...

    work page

  76. [76]

    There is a vertexvin the interior of the context which has a non-local supercolour and such that: a)vis on the left side with respect to some supercolour; and b)vis on the right side with respect to some supercolour

    work page

  77. [77]

    There are verticesv≠win the interior of the context which have non-local supercolours and such that: a)vis on the left side with respect to some supercolour; and b)wis on the right side with respect to the same super- colour; and c) the equivalence from Definition V.12 is violated

    work page

  78. [78]

    There is a path where all vertices are in the interior of the context and: a) the internal vertices (i.e. the vertices that are not the source or target of the path) have local colours; b) the source is on the left side with respect to some supercolour; c) the target is on the right side with respect to some supercolour. Proof.The proof of this claim is e...

    work page

  79. [79]

    Suppose first that the two witness vertices have the same supercolour. This means that there are only two supercolours involved: the supercolourAof the two vertices, and some other entangled supercolourBthat is used to assign the vertices to their sides. Assume without loss of generality thatA→B. Letvbe the vertex on the left side, and letwbe the vertex o...

    work page

  80. [80]

    By flipping edges as in Claim A.71, we can assume without loss of generality that the vertex on the left side has supercolourAand the vertex on the right side has supercolourB

    Suppose now that the two witness vertices have dif- ferent supercolours,AandB, but these supercolours are entangled, with the corresponding orientation being A→B. By flipping edges as in Claim A.71, we can assume without loss of generality that the vertex on the left side has supercolourAand the vertex on the right side has supercolourB. This means that e...

    work page

Showing first 80 references.