QPL 2014 Accepted Papers with Abstracts

Philip Atzemoglou. The dagger lambda calculus
Abstract: We present a novel lambda calculus that casts the categorical approach to the study of quantum protocols into the rich and well established tradition of type theory. Our construction extends the linear typed lambda calculus with a linear negation of "trivialised" De Morgan duality. Reduction is realised through explicit substitution, based on a symmetric notion of binding of global scope, with rules acting on the entire typing judgement instead of on a specific subterm. Proofs of subject reduction, confluence, strong normalisation and consistency are provided, and the language is shown to be an internal language for dagger compact categories.
Andre Ranchin. Depicting qudit quantum mechanics and mutually unbiased qudit theories
Abstract: We generalize the ZX calculus to quantum systems of dimension higher than two. The resulting calculus is sound and universal for quantum mechanics. We define the notion of a mutually unbiased qudit theory and study two particular instances of these theories in detail: qudit stabilizer quantum mechanics and Spekkens-Schreiber toy theory for dits.
The calculus allows us to analyze the structure of qudit stabilizer quantum mechanics and provides a geometrical picture of qudit stabilizer theory using D-toruses, which generalizes the Bloch sphere picture for qubit stabilizer quantum mechanics. We also use our framework to describe generalizations of Spekkens toy theory to higher dimensional systems. This gives a novel proof that qudit stabilizer quantum mechanics and Spekkens-Schreiber toy theory for dits are operationally equivalent in three dimensions.
The qudit pictorial calculus is a useful tool to study quantum foundations, understand the relationship between qubit and qudit quantum mechanics, and provide a novel, high level description of quantum information protocols.
Patrick Coles and Fabian Furrer. Entropic formulation of Heisenberg's measurement-disturbance relation
Abstract: Heisenberg's original intuition was that there should be a tradeoff between measuring a particle's position with greater precision and disturbing its momentum. Recent formulations of this idea have primarily focused on the question of how well two complementary observables can be jointly measured. Here, we provide an alternative approach based on how enhancing the predictability of one observable necessarily disturbs a complementary one. Our measurement-disturbance relation refers to a clear operational scenario and is expressed by entropic quantities with clear statistical meaning, evading recent criticism directed at some previous formulations. We show that our relation is perfectly tight for all measurement strengths in an existing experimental setup involving qubit measurements.
Miriam Backens. The ZX -calculus is approximately complete for single qubits
Abstract: The ZX-calculus is a graphical calculus for reasoning about pure state qubit quantum mechanics. It is complete for pure qubit stabilizer quantum mechanics, meaning any equality involving only stabilizer operations that can be derived using matrices can also be derived pictorially. Yet for general pure state qubit quantum mechanics, the ZX-calculus is incomplete: there exist equalities involving non-stabilizer operations on single qubits which can not be derived from the current rule set for the ZX-calculus. Here, we show that the ZX-calculus for single qubits remains complete upon adding the operator T to the single-qubit stabilizer operations. As any single-qubit operator can be approximated to arbitrary accuracy using only single-qubit stabilizer operations and T, we conclude that the ZX-calculus for single qubits is approximately complete.
Aleks Kissinger and David Quick. Tensors, !-graphs, and non-commutative quantum structures
Abstract: Categorical quantum mechanics (CQM) and the theory of quantum groups rely heavily on the use of structures that have both an algebraic and co-algebraic component, making them well-suited for manipulation using diagrammatic techniques. Diagrams allow us to easily form complex compositions of (co)algebraic structures, and prove their equality via graph rewriting. One of the biggest challenges in going beyond simple rewriting-based proofs is designing a graphical language that is expressive enough to prove interesting properties (e.g. normal form results) about not just single diagrams, but entire families of diagrams. One candidate is the language of !-graphs, which consist of graphs with certain subgraphs marked with boxes (called !-boxes) that can be repeated any number of times. New !-graph equations can then be proved using a powerful technique called !-box induction. However, previously this technique only applied to commutative (or cocommutative) algebraic structures, severely limiting its applications in some parts of CQM and (especially) quantum groups. In this paper, we fix this shortcoming by offering a new semantics for non-commutative !-graphs using an enriched version of Penrose's abstract tensor notation.
Mathys Rennela. Towards a Quantum Domain Theory: Order-enrichment and Fixpoints in W*-algebras
Abstract: We discuss how the theory of operator algebras, also called operator theory, can be applied in quantum computer science. From a computer scientist point of view, we explain some fundamental results of operator theory and their relevance in the context of domain theory. In particular, we consider the category $\wPSU$ of W*-algebras together with normal sub-unital maps, provide an order-enrichment for this category and exhibit a class of its endofunctors with a canonical fixpoint.

Full paper: http://www.cs.ru.nl/~mathysr/papers/quantum-domain-theory.pdf
Eric Cavalcanti and Raymond Lal. On modifications of Reichenbach's principle of common cause in light of Bell's theorem
Abstract: Bell's 1964 theorem causes a severe problem for the notion that correlations require explanation, encapsulated in Reichenbach's Principle of Common Cause. Despite being a hallmark of scientific thought, dropping the principle has been widely regarded as a much less bitter medicine than the perceived alternative---dropping relativistic causality. Recently, however, some authors have proposed that modified forms of Reichenbach's principle could be maintained even with relativistic causality. Here we break down Reichenbach's principle into two independent assumptions---the Principle of Common Cause proper, and Factorisation of Probabilities. We show how Bell's theorem can be derived from these two assumptions plus relativistic causality and the Law of Total Probability for actual events, and we review proposals to drop each of these assumptions in light of the theorem. In particular, we show that the 'non-commutative common causes' of Hofer-Szabo and Vecsernyes fail to have an analogue of the notion that the common causes can explain the observed correlations. Moreover, we show that their definition can be satisfied trivially by any quantum product state for any quantum correlations. We also discuss how the conditional states approach of Leifer and Spekkens fares in this regard.
Bob Coecke. Normalisation equals non-signalling
Abstract: The notions of normalisation and non-signalling coincide for general process theories, provided one makes causal structure explicit, which is unavoidable to even make sense of the notion of non-signalling. Because of its much simpler mathematical form, normalisation (which is equivalent to the Pavia's causality-axiom) should therefore be taken to be more fundamental than non-signalling.
Nadish de Silva. Contextuality and Noncommutative Geometry
Abstract: We report on progress on our attempt to generalize the notion of the Gel'fand spectrum of commutative $C^*$-algebras to a notion of spectrum for not-necessarily-commutative $C^*$-algebras in a fashion modelled on Isham and Butterfield's geometric reformulation of the Kochen-Specker theorem. By synthesizing the insights of noncommutative geometers with those of physicists concerned with contexuality in quantum theory, we hope to gain deeper structural understanding of noncommutative geometry and provide automatic generalizations of classical concepts to contextual physical theories other than quantum mechanics.

After briefly reviewing a novel definition of operator $K$-theory given in terms of an extension of topological $K$-theory, we report on recent progress on a conjecture made at QPL 2013: an extension of the functor assigning to a topological space its lattice of closed sets yields the functor which assigns to a $C^*$-algebra its lattice of closed, two-sided ideals. This is tantamount to recovering the Jacobson topology on the primary ideal spectrum of an arbitrary $C^*$-algebra as the limit of topologies coming from the algebra's contexts. Together with Rui Soares Barbosa, we prove the von Neumann algebraic analogue of the conjecture (a significant step towards proving the full conjecture) and, in doing so, answer a question of Heunen and Reyes by identifying precisely which partial ideals of a von Neumann algebra arise from total ideals.
Antonin Delpeuch. Complexity of Grammar Induction for Quantum Types
Abstract: Most categorical models of meaning use a functor from the syntactic category to the semantic category. When semantic information is available, the problem of grammar induction can therefore be defined as finding preimages of the semantic types under this forgetful functor, lifting the information flow from the semantic level to a valid reduction at the syntactic level. We study the complexity of grammar induction, and show that for a variety of quantum type systems, including pivotal and compact closed categories, the grammar induction problem is NP-complete. Our approach could be extended to linguistic type systems such as autonomous or bi-closed categories.
Kazuya Yasuda, Takahiro Kubota and Yoshihiko Kakutani. Observational Equivalence Using Schedulers for Quantum Processes
Abstract: In the study of quantum process algebras, researchers have introduced different notions of equivalence between quantum processes like bisimulation or barbed congruence. However, there are intuitively equivalent quantum processes that these notions do not regard as equivalent.
In this paper, we introduce a notion of equivalence named observational equivalence into qCCS. Since quantum processes have both probabilistic and nondeterministic transitions, we introduce schedulers that solve nondeterministic choices and obtain probability distribution of quantum processes.
By definition, the restrictions of schedulers change observational equivalence. We propose some definitions of schedulers, and investigate the relation between the restrictions of schedulers and observational equivalence.
Patrick Coles, Jedrzej Kaniewski and Stephanie Wehner. Equivalence of wave-particle duality to entropic uncertainty
Abstract: Interferometers capture a basic mystery of quantum mechanics: a single quantum particle can exhibit wave behavior, yet that wave behavior disappears when one tries to determine the particle's path inside the interferometer. This idea has been formulated quantitively as an inequality, e.g., by Englert and Jaeger, Shimony, and Vaidman, which upper bounds the sum of the interference visibility and the path distinguishability. Such wave-particle duality relations (WPDRs) are often thought to be conceptually inequivalent to Heisenberg's uncertainty principle, although this has been debated. Here we show that WPDRs correspond precisely to a modern formulation of the uncertainty principle in terms of entropies, namely the min- and max-entropies. This observation unifies two fundamental concepts in quantum mechanics. Furthermore, it leads to a robust framework for deriving novel WPDRs by applying entropic uncertainty relations to interferometric models. As an illustration, we derive a novel relation that captures the coherence in a quantum beam splitter.
Sam Staton. An equational characterization of quantum computation
Abstract: We provide an equational theory describing the algebraic structure of quantum computation. This is inspired by the work by Plotkin, Power and others on using equational theories to describe notions of computation. We show that our axioms are complete with respect to the interpretation as completely positive maps between C*-algebras.
Chris Heunen, Jamie Vicary and Linde Wester. Mixed quantum states in higher categories
Abstract: There are two ways to describe the interaction between classical and quantum information categorically: one based on completely positive maps between Frobenius algebras, the other using symmetric monoidal 2-categories. This paper makes a first step towards combining the two. The integrated approach allows a unified description of quantum teleportation and classical encryption in a single 2-category, as well as a universal security proof applicable simultaneously to both scenarios.
Krzysztof Bar and Jamie Vicary. A 2-Categorical Analysis of Complementary Families, Quantum Key Distribution and the Mean King Problem
Abstract: This paper explores the use of 2-categorical technology for describing and reasoning about complex quantum procedures. We give syntactic definitions of a family of complementary measurements, and of quantum key distribution, and show that they are equivalent. We then show abstractly that either structure gives a solution to the Mean King problem, which we also formulate 2-categorically.
Shane Mansfield. Reflections on the PBR Theorem: Reality Criteria & Preparation Independence
Abstract: This paper contains initial work on attempting to bring recent developments in the foundations of quantum mechanics concerning the nature of the wavefunction within the scope of more logical and structural methods. A first step involves dualising a criterion for the reality of the wavefunction proposed by Harrigan & Spekkens, which was central to the Pusey-Barrett-Rudolph theorem. The resulting criterion has several advantages, including the avoidance of certain technical difficulties relating to sets of measure zero. By considering the `reality' not of the wavefunction but of the observable properties of any ontological physical theory a new characterisation of non-locality and contextuality is found. Secondly, a careful analysis of preparation independence, one of the key assumptions of the PBR theorem, leads to a precise analogy with the kind of locality prohibited by Bell's theorem. Motivated by this, we propose a weakening of the assumption to something analogous to no-signalling. This amounts to allowing global or non-local correlations in the joint ontic state, which nevertheless do not allow for superluminal signalling. This is, at least, consistent with the Bell and Kochen-Specker theorems. We find a counter-example to the PBR argument, which violates preparation independence, but does satisfy this physically motivated assumption. The question of whether the PBR result can be strengthened to hold under the relaxed assumption is therefore posed.
William Zeng and Jamie Vicary. Abstract structure of unitary oracles for quantum algorithms
Abstract: We show that a pair of complementary dagger-Frobenius algebras, equipped with a self-conjugate comonoid homomorphism onto one of the structures, produce a nontrivial unitary morphism on the product of the algebras. This gives an abstract understanding of the structure of an oracle in a quantum computation, and we apply this to develop a new algorithm for deterministic identification of group homomorphisms into abelian groups. We also discuss an application to the categorical theory of signal-flow networks.
Quanlong Wang and Xiaoning Bian. Dichromatic and Trichromatic Calculus for Qutrit Systems
Abstract: We introduce a dichromatic calculus and a trichromatic calculus for qutrit systems. We give a translation functor from the category of dichromatic graphs to the category of trichromatic graphs. We also show that the decomposition of the qutrit Hadamard gate is not derivable from the dichromatic calculus without K2 rules.
Joe Henson, Raymond Lal and Matthew Pusey. General probabilistic theories on arbitrary causal structures
Abstract: Bayesian networks provide a powerful tool for reasoning about probabilistic causation, used in many areas of science. They are, however, intrinsically classical. In particular, Bayesian networks naturally yield the Bell inequalities. Inspired by this connection, we generalise the formalism of classical Bayesian networks in order to investigate non-classical correlations in arbitrary causal structures. Our framework of `generalised Bayesian networks' replaces latent variables with the resources of any generalised probabilistic theory, most importantly quantum theory, but also, for example, Popescu-Rohrlich boxes. We obtain three main sets of results. Firstly, we prove that all of the observable conditional independences required by the classical theory also hold in our generalisation; to obtain this, we extend the classical d-separation theorem to our settting. Secondly, we find that the theory-independent constraints on probabilities can go beyond these conditional independences. For example we find that no probabilistic theory predicts perfect correlation between three parties using only bipartite common causes. Finally, we begin a classification of those causal structures, such as the Bell scenario, that may yield a separation between classical, quantum and general-probabilistic correlations.
Dimitri Kartsaklis and Mehrnoosh Sadrzadeh. A Study of Entanglement in a Categorical Framework of Natural Language
Abstract: In both quantum mechanics and corpus linguistics based on vector spaces, the notion of entanglement provides a means for the various subsystems to communicate with each other. In this paper we examine a number of implementations of the categorical framework of Coecke et al. (2010) for natural language, from an entanglement perspective. Specifically, our goal is to better understand in what way the level of entanglement of the relational tensors (or the lack of it) affects the compositional structures in practical situations. Our findings reveal that a number of proposals for verb construction lead to almost separable tensors, a fact that considerably simplifies the interactions between the words. We examine the ramifications of this fact, and we show that the use of Frobenius algebras mitigates the potential problems to a great extent. Finally, we briefly examine a machine learning method that creates verb tensors exhibiting a sufficient level of entanglement.
Christian Schröder de Witt and Vladimir Zamdzhiev. The ZX calculus is incomplete for quantum mechanics
Abstract: We prove that the ZX-calculus is incomplete for quantum mechanics. We suggest the addition of a new ’color-swap’ rule, of which currently no analytical formulation is known and which we suspect may be necessary, but not sufficient to make the ZX-calculus complete.
Jason Morton. Belief propagation in monoidal categories
Abstract: We discuss a categorical version of the celebrated belief propagation algorithm. This makes some algorithms known or suspected to be analogous actually identical, and highlights the computational point of view in monoidal categories.
Jisho Miyazaki, Michal Hajdusek and Mio Murao. Translating measurement-based quantum computations with gflow into quantum circuits
Abstract: Causal flow (flow) and generalized flow (gflow) are ordering relations on a graph state that guarantee deterministic implementations of a unitary by measurement-based quantum computation (MBQC).
%A translation method for a unitary described by MBQC to a quantum circuit model was known only for graphs with flow, since a straightforward extension of the method to graphs with gflow leads to a circuit including acausal gates, which is not well-defined in the quantum circuit model.
There is a method called star pattern transformation to write a circuit decomposition of a unitary described by MBQC on a graph with flow.
The straight extension of this method onto graphs with gflow, however, leads to a circuit including acausal gates, which is not well-defined in the quantum circuit model.
In this work, we present a generalized method to translate any unitary implemented by MBQC with gflow into a quantum circuit without dealing with acausal gates. We also present another translation method that first maps to a quantum circuit including acausal gates and then erasing them to obtain an ordinary quantum circuit.
By comparing these two methods, we study how the depth of quantum computation can be compressed in MBQC compared to the quantum circuit model.
This QPL2014 submission is based on the work arXiv:1310.4043.
Rui Soares Barbosa. On monogamy of non-locality and macroscopic averages: examples and preliminary results
Abstract: We explore a connection between monogamy of non-locality and a weak macroscopic locality condition: the locality of the average behaviour. These are revealed by our analysis as being two sides of the same coin.

Moreover, we exhibit a structural reason for both in the case of Bell-type multipartite scenarios, shedding light on but also generalising the results in the literature [Ramanathan et al. (2011), Pawłowski & Brukner (2009)]. More specifically, we show that, provided the number of particles in each site is large enough compared to the number of allowed measurement settings, and whatever the microscopic state of the system, the macroscopic average behaviour is local realistic, or equivalently, general multipartite monogamy relations hold.

This result relies on a classical mathematical theorem by Vorob’ev (1962) about extending compatible families of probability distributions defined on the faces of a simplicial complex - in the language of the sheaf-theoretic framework of Abramsky and Brandenburger (2011), such families correspond to no-signalling empirical models, and the existence of such extension corresponds to locality/non-contextuality. Since Vorob’ev’s theorem depends solely on the structure of the simplicial complex (i.e. the compatibility of the measurements) and not on the specific probability distributions (i.e. the empirical models), our result about monogamy relations and locality of macroscopic averages holds true not just for quantum theory, but for any empirical model satisfying the no-signalling condition.

In this extended abstract, we illustrate this result by working out a couple of examples that convey the intuition behind our analysis while keeping the discussion at an elementary level.
Kohei Kishida. Stochastic Relational Presheaves and Dynamic Logic for Contextuality
Abstract: Presheaf models provide a formulation of labelled transition systems that is useful for, among other things, modelling concurrent computation. This paper aims to extend such models further to represent stochastic dynamics such as shown in quantum systems. After reviewing what presheaf models represent and what certain operations on them mean in terms of notions such as internal and external choices, composition of systems, and so on, I will show how to extend those models and ideas by combining them with ideas from other category-theoretic approaches to relational models and to stochastic processes. It turns out that my extension yields a transitional formulation of sheaf-theoretic structures that Abramsky and Brandenburger (2011) proposed to characterize non-locality and contextuality. An alternative characterization of contextuality will then be given in terms of a dynamic modal logic of the models I put forward.
Akihito Soeda, Shojun Nakayama and Mio Murao. Circuit model implementation of controllization functional on unitary with and without fractional query
Abstract: High-level programming languages aim to provide an intuitive interface to programmers, typically, via uses of functionals (or a function of a function), a trend already seen in quantum programming. Since a unitary itself is a function on quantum states, a function that maps a given unitary to its controlled counterpart (namely, the controlled-unitary) is a functional in quantum computation. We prove that such a ``controllization" functional is NOT implementable as a quantum circuit, even if we consider implementations using multiple queries to the input unitary, with non-deterministic success probability, and an extra degree of freedom in the relative phase of the controlled unitary. We show, however, with fractional unitary queries and their inverse, probabilistic controllization is possible with multiple calls and the degree of freedom in the relative phase. In addition, it is proven that the inverse query is unnecessary for single-qubit unitaries, by presenting a circuit that implements the inverse query exactly but probabilistically with a single query of the input unitary. Our result shows that the circuit model becomes provably more powerful with fractional queries in the circuit implementation of quantum functionals.
Toru Takisaka. On Gacs' quantum algorithmic entropy
Abstract: We define an infinite dimensional modification of lower-semicomputability of density operators by G\'acs, and examine their properties, especially the well-definedness of his quantum algorithmic entropy. It turns out that showing the existence of universal operator is not so easy, but once we show this we can get an analogous consequence in G\'acs. We also show that universal operator has certain untrivial form if it exists.
Mio Murao, Kousuke Nakago, Michal Hajdusek and Shojun Nakayama. Parallelized adiabatic gate teleportation
Abstract: To investigate how a causally ordered gate sequence can be parallelized in adiabatic implementations of quantum computation, we extend adiabatic gate teleportation (AGT), a model of quantum computation recently proposed by D. Bacon and S.~T. Flammia, Phys. Rev. Lett. {\bf 103}, 120504 (2009), to a form deterministically simulating parallelized gate teleportation, which is achievable only by postselection. We introduce a {\it twisted Hamiltonian}, which is a Hamiltonian of the Heisenberg-type interaction where the coordinates of the second qubit is twisted according to a unitary gate. We develop {\it parallelized adiabatic gate teleportation} (PAGT) where a sequence of unitary gates is performed in a single step of the adiabatic process. In PAGT, the necessary time for the adiabatic evolution implementing a sequence of gates increases quadratically, however it maps causal order of gates to spatial order of interactions specified by the final Hamiltonian. Using this property, we present a controlled-PAGT scheme to manipulate the order of gates by a control-qubit. In the controlled-PAGT scheme, two differently ordered unitary operations $GF$ and $FG$ are coherently performed depending on the state of a control-qubit by simultaneously applying the twisted Hamiltonians of $F$ and $G$. We show that the twisted Hamiltonian has an ability to perform the transposed unitary gate in addition to the unitary gate and time reverse transformations represented by the transposed unitary gate enable deterministic simulation of an postselected event of parallelized gate teleportation. The details are presented in arXiv:1310.4061.
Seiseki Akibue, Masaki Owari, Go Kato and Mio Murao. Globalness of separable maps in terms of time and space resources
Abstract: We propose a new approach to analyze globalness of separable maps and to distinguish them from local operations and classical communications (LOCC) and non-separable maps. In this approach, all quantum operations are restricted in the local spaces, but classical communication connecting different times (super communication) described by fictitious acausal classical correlations without globally causal structure can be used as additional resources relaxing LOCC constraints on time. We define a map described by local operations and super communication (LOSC) and prove that the intersection of the set of LOSC and the set of completely positive trace preserving (CPTP) maps is equivalent to the set of separable maps. We show that LOSC is closely related to the framework of the process matrix introduced by Oreshkov et. al. for analyzing quantum correlations with no causal order. We also investigate the gap between separable maps and LOCC in a conventional approach, by analyzing the amount of entanglement , which relaxes LOCC constraints on space, required in entanglement assisted LOCC implementations of separable maps for the orthogonal basis state dis- crimination problems. Combining these two approaches, the globalness of separable maps can be interpreted as a correspondence between the time and space resources, namely, acausal classical correlations and entanglement.
Shane Mansfield. Completeness of Hardy Non-locality: Consequences \& Applications
Abstract: Completeness results due to Mansfield & Fritz show that Hardy's paradox provides a necessary and sufficient condition for logical non-locality in all (2,2,l) and (2,k,2) scenarios. This paper considers a variety of consequences and applications of these results. This includes a proof that Bell states, despite being perhaps the most studied and utilised of entangled states, appear to be anomalous in terms of non-locality, in the sense that they are the only entangled two-qubit states which are not logically non-local. Much of the literature on Hardy's paradox is concerned with the probability of witnessing a paradox, which has experimental motivations: the highest probability to date is approximately 0.4, which is achieved by a model proposed by Chen et al. We achieve a striking improvement on this, demonstrating that it is possible to witness Hardy non-locality with certainty for a tripartite quantum system. We also discuss results relating to strong non-locality, and to the complexity of logical non-locality.
Robin Adams. QPEL: Quantum Program and Effect Language
Abstract: We present the syntax and rules of deduction of QPEL (Quantum Program and Effect Language), a language for describing both quantum programs, and properties of quantum programs - effects on the appropriate Hilbert space. We show how semantics may be given in terms of state-and-effect triangles, a categorical setting that allows semantics in terms of Hilbert spaces, C$^*$-algebras, and other categories. We prove soundness and completeness results that show the derivable judgements are exactly those provable in all state-and-effect triangles.
Kenta Cho. Semantics for a Quantum Programming Language by Operator Algebras
Abstract: This paper presents a novel semantics for a quantum programming language by operator algebras, which are known to give a formulation for quantum theory that is alternative to the one by Hilbert spaces. We show that the opposite category of the category of W*-algebras and normal completely positive pre-unital maps is an elementary quantum flow chart category in the sense of Selinger. As a consequence, it gives a denotational semantics for Selinger’s first-order functional quantum programming language QPL. The use of operator algebras allows us to accommodate infinite structures and to handle classical and quantum computations in a unified way.
Bas Westerbaan and Sander Uijlen. A Kochen-Specker system has at least 21 vertices
Abstract: At the heart of the Conway’s Free Will theorems and Kochen and Specker’s argument against noncontextual hidden variable theories is the existence of a Kochen-Specker (KS) system: a set of points on the sphere that has no {0, 1}-coloring such that at most one of two orthogonal points are colored 1 and of three pairwise orthogonal points exactly one is col- ored 1. In public lectures, Conway encouraged the search for small KS systems. At the time of writing, the smallest known KS system has 31 vectors.
Arends, Ouaknine and Wampler have shown that a KS system has at least 18 vectors, by reducing the problem to the existence of graphs with a topological embeddability and non-colorability property. The bottleneck in their search proved to be the sheer number of graphs on more than 17 vertices and deciding embeddability.
Continuing their effort, we prove a restriction on the class of graphs we need to consider and develop a more practical decision procedure for embeddability to improve the lower bound to 21.