Short proofs of the Kneser-Lovász coloring principle

ARTICLE IN PRESS UNCORRECTED PROOF Please cite this article in press as: J. Aisenberg et al., Short proofs of the Kneser–Lovász coloring principle, Inf. Comput. (2018), https://doi.org/10.1016/j.ic.2018.02.010 JID:YINCO AID:4352 /FLA [m3G; v1.230; Prn:8/02/2018; 13:15] P.1 (1-15) Information and Computation ••• (••••)•••–••• Contents lists available at ScienceDirect Information and Computation www.elsevier.com/locate/yinco 1 1 2 2 3 3 4 4 5 5 6 6 7 7 8 8 9 9 10 10 11 11 12 12 13 13 14 14 15 15 16 16 17 17 18 18 19 19 20 20 21 21 22 22 23 23 24 24 25 25 26 26 27 27 28 28 29 29 30 30 31 31 32 32 33 33 34 34 35 35 36 36 37 37 38 38 39 39 40 40 41 41 42 42 43 43 44 44 45 45 46 46 47 47 48 48 49 49 50 50 51 51 52 52 53 53 54 54 55 55 56 56 57 57 58 58 59 59 60 60 61 61 Short proofs of the Kneser–Lovász coloring principle ✩ James Aisenberg a,1, Maria Luisa Bonet b,2, Sam Buss a,1,3, Adrian Cr˘ aciun c,4, Gabriel Istrate c,4 aDepartment of Mathematics, University of California, San Diego, La Jolla, CA 92093-0112, USA bComputer Science Department, Universidad Politécnica de Cataluña, Barcelona, Spain cWest University of Timi¸soara, and the e-Austria Research Institute, Timi¸soara, RO-300223, Romania a r t i c l e i n f o a b s t r a c t Article history: Received 31 July 2015 Available online xxxx We prove that propositional translations of the Kneser–Lovász theorem have polynomial size extended Frege proofs and quasi-polynomial size Frege proofs for all fixed values of k. We present a new counting-based combinatorial proof of the Kneser–Lovász theorem based on the Hilton–Milner theorem; this avoids the topological arguments of prior proofs for all but finitely many base cases. We introduce new “truncated Tucker lemma” principles, which are miniaturizations of the octahedral Tucker lemma. The truncated Tucker lemma implies the Kneser–Lovász theorem. We show that the k=1 case of the truncated Tucker lemma has polynomial size extended Frege proofs. 2018 Published by Elsevier Inc. 1. Introduction This paper discusses proofs of Lovász’s theorem about the chromatic number of Kneser graphs and the proof complexity of propositional translations of the Kneser–Lovász theorem. Our main results give a new proof of the Kneser–Lovász theorem, which, for fixed parameter k, uses a simple counting argument based on the Hilton–Milner theorem in place of the topological arguments used in prior proofs, for all but finitely many cases. These arguments can be formalized in propositional logic to give polynomial size extended Frege proofs and quasi-polynomial size Frege proofs. The proof complexity of Frege and extended Frege systems was first studied by Cook and Reckhow [14,15] and Statman [31]. Frege systems (denoted F) are sound and complete proof systems for propositional logic with a finite set of schemes for axioms and inference rules. The typical example is a “textbook style” propositional proof system using modus ponens as its only rule of inference. In fact, all Frege systems are equivalent to this system [15]. Extended Frege systems (denoted eF) are Frege systems augmented with the extension rule, which allows variables to abbreviate complex formulas. The reader unfamiliar with Frege systems can consult the surveys [6,11,12,15,24,30] for more information. ✩This is an expanded version of a paper [3] which appeared in ICALP 2015. E-mail addresses: [email protected] (J. Aisenberg), [email protected] (M.L. Bonet), [email protected] (S. Buss), [email protected] (A. Cr˘ aciun), gabrielistr[email protected] (G. Istrate). 1Supported in part by NSF grants DMS-1101228 and CCF-1213151. Part of this work was carried out while visiting St. Petersburg with support from the Skolkovo Institute of Technology. 2Supported in part by grant TIN2013-48031-C4-1. 3Supported in part by Simons Foundation award 306202. 4Supported in part by IDEI grant PN-II-ID-PCE-2011-3-0981 “Structure and computational difficulty in combinatorial optimization: an interdisciplinary approach”. https://doi.org/10.1016/j.ic.2018.02.010 0890-5401/2018 Published by Elsevier Inc. © 2018 Elsevier. This manuscript version is made available under the CC-BY-NC-ND 4.0 license http://creativecommons.org/licenses/by-nc-nd/4.0/ ARTICLE IN PRESS UNCORRECTED PROOF Please cite this article in press as: J. Aisenberg et al., Short proofs of the Kneser–Lovász coloring principle, Inf. Comput. (2018), https://doi.org/10.1016/j.ic.2018.02.010 JID:YINCO AID:4352 /FLA [m3G; v1.230; Prn:8/02/2018; 13:15] P.2 (1-15) 2J. Aisenberg et al. / Information and Computation ••• (••••)•••–••• 1 1 2 2 3 3 4 4 5 5 6 6 7 7 8 8 9 9 10 10 11 11 12 12 13 13 14 14 15 15 16 16 17 17 18 18 19 19 20 20 21 21 22 22 23 23 24 24 25 25 26 26 27 27 28 28 29 29 30 30 31 31 32 32 33 33 34 34 35 35 36 36 37 37 38 38 39 39 40 40 41 41 42 42 43 43 44 44 45 45 46 46 47 47 48 48 49 49 50 50 51 51 52 52 53 53 54 54 55 55 56 56 57 57 58 58 59 59 60 60 61 61 The size of a Frege or extended Frege proof is the number of symbols in the proof. A proof system P1simulates a proof system P2if and only if there is a polynomial p(n)such that, for any propositional formula ϕ, if ϕhas a P2-proof of size n, then ϕhas a P1-proof of size ≤p(n). Also, P1quasi-polynomially simulates P2if and only if there is a k>0 such that, if ϕhas a P2-proof of size nthen ϕhas a P1-proof of size ≤2(log n)k. It is trivial that extended Frege systems simulate Frege systems. It is generally conjectured that the extension rule can provide substantial shortening of proof length, and therefore that Frege systems do not (quasi-polynomially) simulate extended Frege systems. The intuition is that Frege proofs are able to reason using Boolean formulas; whereas extended Frege proofs can reason using Boolean circuits (see [22]). Boolean formulas are conjectured to require exponential size to simulate Boolean circuits. There is no known direct connection to proof complexity, but it is generally conjectured by analogy that there is an exponential separation between the sizes of Frege proofs and extended Frege proofs, and thus that Frege systems do not (quasi-polynomially) simulate extended Frege systems. Bonet, Buss, and Pitassi [6] systematically looked for combinatorial tautologies that could be candidates for exponentially separating proof sizes for Frege and extended Frege systems. Surprisingly, they found only a small number. The first candidates were based on linear algebra, including the Oddtown theorem, the Graham–Pollack theorem, the Fisher Inequality, the Ray–Chaudhuri–Wilson theorem, and the AB =I⇒B A =Itautology (the last was suggested by S. Cook). The remaining candidate was Frankl’s theorem on the trace of sets. All of these principles were shown to have polynomial size extended Frege proofs, but it was open whether they had polynomial size Frege proofs. Hrubeš and Tzameret [20] recently showed that the five tautologies based on linear algebra have quasi-polynomial size Frege proofs by showing that there are quasi-polynomial size definitions of determinants whose properties can be established by quasi-polynomial Frege proofs (as was conjectured by [6]). Subsequently, Aisenberg, Bonet, and Buss [2] proved that Frankl’s theorem also has quasi-polynomial size Frege proofs. With these results, none of the principles considered by Bonet–Buss–Pitassi provide an exponential separation of Frege and extended Frege systems. An earlier combinatorial candidate was the pigeonhole principle, introduced by Cook and Reckhow [15]. They showed this has polynomial size extended Frege proofs. Buss [9] later proved this also has polynomial size Frege proofs. Buss’s proof was based on “counting”, and established that Frege proofs can use polynomial size formulas (based on carry-save addition) to define sizes of sets, and can reason about sizes effectively. Carry-save addition also allows Frege systems to reason about integer multiplication and about adding vectors of integers. The ability of Frege proofs to “count” and to reason about sizes of sets will be important for our Frege proofs of the Kneser–Lovász theorem. The counting proofs were quite different than Cook and Reckhow’s inductive proofs of the pigeonhole principle, so these were sometimes taken as evidence that Frege systems do not (quasi-polynomially) simulate extended Frege proofs. However, [7] recently showed that Cook and Reckhow’s inductive proofs can be reformulated as quasi-polynomial size Frege proofs. Another class of candidates is based on consistency statements. We write ConP(n)for the propositional statement expressing the condition that the proof system Pdoes not have a proof of p∧ ¬pof size ≤n. For “natural” systems P (including Frege and extended Frege systems), the formula ConP(n)has size polynomially bounded by n(e.g., [13,10]). Propositional consistency statements have been studied for first-order systems by Pudlák [28,29] and Friedman [unpublished]. Pudlák showed that axiomatizable theories of arithmetic have polynomial size (first-order) proofs of their partial consistency statements; Pudlák and Friedman independently proved polynomial lower bounds as well. Cook [13] showed that an extended Frege system has polynomial size proofs of its own partial consistency statements ConeF(n). Buss [10] proved similarly that a Frege system has polynomial size proofs of its partial consistency statements ConF(n). It also follows from [10] that Frege systems (quasi-)polynomially simulate extended Frege systems iff there are (quasi-)polynomial size Frege proofs of ConeF(n). In addition, ConeF(n)is a “logical” principle not really a “combinatorial” principle.5For these reasons, partial consistency statements such as ConeF(n)do not serve as the kinds of candidates for separating Frege and extended Frege system that we are seeking. Other candidates for exponentially separating Frege and extended Frege systems arose from the work of Kołodziejczyk, Nguyen, and Thapen [23] in the setting of bounded arithmetic [8]. These include various forms of the local improvement principles LI, LIlog and LLI. The results of [23] showed that the LI principle is many-one complete for the NP search problems of V1 2; it follows that LI is equivalent to partial consistency statements for extended Frege systems. Beckmann and Buss [5] subsequently proved that LIlog is provably equivalent (in S1 2) to LI and that the linear local improvement principle LLI is provable in U1 2. The LLI principle thus has quasi-polynomial size Frege proofs. Combining the results of [5,23] shows that LIlog and LLI are many-one complete for the NP search problems of V1 2and U1 2, respectively, and thus equivalent to partial consistency statements for extended Frege and Frege systems, respectively. Thus, apart from partial consistency statement, none of the above principles serve as combinatorial candidates for showing that Frege systems do not quasi-polynomially simulate extended Frege systems. A new candidate based on the Kneser–Lovász theorem was recently proposed by Istrate and Cr˘ aciun [21]. As defined below, the Kneser–Lovász theorem gives a lower bound on the chromatic of the (n,k)-Kneser graphs. Istrate and Cr˘ aciun showed that the k=3 case of these tautologies have polynomial size extended Frege proofs, but left open whether they 5However, see Avigad [4] for a combinatorial version of ConeF(n). ARTICLE IN PRESS UNCORRECTED PROOF Please cite this article in press as: J. Aisenberg et al., Short proofs of the Kneser–Lovász coloring principle, Inf. Comput. (2018), https://doi.org/10.1016/j.ic.2018.02.010 JID:YINCO AID:4352 /FLA [m3G; v1.230; Prn:8/02/2018; 13:15] P.3 (1-15) J. Aisenberg et al. / Information and Computation ••• (••••)•••–••• 3 1 1 2 2 3 3 4 4 5 5 6 6 7 7 8 8 9 9 10 10 11 11 12 12 13 13 14 14 15 15 16 16 17 17 18 18 19 19 20 20 21 21 22 22 23 23 24 24 25 25 26 26 27 27 28 28 29 29 30 30 31 31 32 32 33 33 34 34 35 35 36 36 37 37 38 38 39 39 40 40 41 41 42 42 43 43 44 44 45 45 46 46 47 47 48 48 49 49 50 50 51 51 52 52 53 53 54 54 55 55 56 56 57 57 58 58 59 59 60 60 61 61 have (quasi-)polynomial size Frege proofs. However, the main results of the present paper show that, for any fixed k≥1, the Kneser–Lovász tautologies have quasi-polynomial size Frege proofs. Thus these also do not give an exponential separation of Frege from extended Frege systems. With these last results, we have few remaining combinatorial candidates for showing Frege systems do not quasipolynomially simulate extended Frege systems. One remaining candidate is tautologies based on the Rectangular Local Improvement principles, RLIk, of Beckmann–Buss [5] for fixed k≥2. The only other combinatorial candidate we know of is introduced in Section 6 below. This is the k=1 case of the “truncated Tucker lemma”. Theorem 25 shows it has polynomial size extended Frege proofs; however, we have been unable to show that it has quasi-polynomial size Frege proofs. The outline of the paper is as follows. First, in Section 2 we define the (n,k)-Kneser graphs and state Lovász’s theorem about their chromatic numbers. Theorems 4 and 5 state our main results about Frege and extended Frege proofs of that theorem. Section 3 gives an informal (“mathematical”) proof of the Kneser–Lovász theorem using a new proof method based on a simple counting argument. Prior proofs used, at least implicitly, a topological fixed-point lemma. The most combinatorial proof is by Matoušek [26] and is inspired by the octahedral Tucker lemma; see also Ziegler [32]. Our new proofs mostly avoid topological arguments and use a counting argument instead. The counting arguments are used to prove the existence of “star-shaped” color classes. These counting arguments can be formalized with Frege proofs. For the Kneser–Lovász theorem, the counting arguments reduce the general case to “small” instances of size n≤2k4. For fixed k, there are only finitely many small instances, and they can be verified by exhaustive enumeration. As we shall see, this leads to polynomial size extended Frege proofs, and quasi-polynomial size Frege proofs for the Kneser–Lovász principles. Sections 3.1 and 3.2 give two “mathematical” versions of the counting proofs, which will be formalized as extended Frege proofs and Frege proofs (respectively). Section 3.3 is a short diversion and considers whether there are colorings of the Kneser graphs with many non-starshaped color classes. Section 4 discusses some of the details of formalizing the arguments in Section 3 in the Frege and extended Frege systems, establishing our two main theorems. We focus on expressing the concepts described in Section 3 in propositional logic, and we only sketch some of the details of how Frege systems can prove properties of these concepts. The proofs of the Kneser–Lovász theorem in Sections 3 and 4 reduce the general case of the Kneser–Lovász theorem to finitely many base cases, which are then handled by exhaustive enumeration. It would be interesting to give a uniform proof that does not need to handle the base cases in this way. Motivated by this, Section 5 defines new “truncated” forms of the octahedral Tucker lemma. These truncated Tucker lemmas can be expressed as families of polynomial size propositional tautologies. The octahedral Tucker lemma, on the other hand, can only be expressed by exponential size formulas. Matoušek showed that the Kneser–Lovász theorem follows from the octahedral Tucker lemma. We refine this by proving that the octahedral Tucker lemma implies the two truncated Tucker lemmas, that the two versions of the truncated Tucker lemma are equivalent, and that the truncated Tucker lemmas imply the Kneser–Lovász theorem. Since the truncated Tucker lemmas can be expressed as polynomial size tautologies, it is natural to ask about their proof complexity in (extended) Frege systems. Section 6 establishes that the k=1 cases of the truncated Tucker lemmas have polynomial size extended Frege proofs. It is open whether these have (quasi-)polynomial size Frege proofs. Thus, this is a candidate for separating Frege and extended Frege systems. Likewise, it is open whether the truncated Tucker lemmas for k>1 have subexponential size extended Frege proofs. For this, it is tempting to try to modify the combinatorial proof of the Tucker lemma of Freund and Todd [18] (see also Matoušek [26]). Their proof uses a version of the parity principle PPA [27]. In fact, the general (not necessarily octahedral) Tucker lemma is known to be many-one complete for PPA [1]. However, Freund and Todd’s proof applies the parity principle to exponentially large graphs, and this prevents us from directly formalizing their arguments with polynomial size extended Frege proofs. We thank the two referees for helpful comments and suggestions. 2. The Kneser–Lovász principle and statement of the main theorems The (n,k)-Kneser graph is defined to be the undirected graph whose vertices are the k-subsets of {1, . . . ,n}; there is an edge between two vertices iff those vertices have empty intersection. The Kneser–Lovász theorem states that Kneser graphs have a large chromatic number: Theorem 1 (Lovász [25]). Let n≥2k>1. The (n,k)-Kneser graph has no coloring with n−2k+1colors. It is well-known that the (n,k)-Kneser graph has a coloring with n−2k+2 colors (see Section 3.3), so the bound n−2k+1 is optimal. For k=1, the Kneser–Lovász theorem is just the pigeonhole principle. Istrate and Cr˘ aciun [21] noted that, for fixed values of k, the propositional translations of the Kneser–Lovász theorem are polynomial size in n. They presented proofs that can be formalized by polynomial size Frege proofs for k=2, and by polynomial size extended Frege proofs for k=3. This left open the possibility that the k=3 case could exponentially separate the Frege and extended Frege systems. It was also left open whether the k>3 case of the Kneser–Lovász theorem gave tautologies that require exponential size extended Frege proofs. As discussed above, the present paper refutes these possibilities. Theorems 4 and 5 summarize these results. Let [n]be the set {1, . . . ,n}; members of [n]are called nodes. We identify n kwith the set of k-subsets of [n], the vertices of the (n,k)-Kneser graph. ARTICLE IN PRESS UNCORRECTED PROOF Please cite this article in press as: J. Aisenberg et al., Short proofs of the Kneser–Lovász coloring principle, Inf. Comput. (2018), https://doi.org/10.1016/j.ic.2018.02.010 JID:YINCO AID:4352 /FLA [m3G; v1.230; Prn:8/02/2018; 13:15] P.4 (1-15) 4J. Aisenberg et al. / Information and Computation ••• (••••)•••–••• 1 1 2 2 3 3 4 4 5 5 6 6 7 7 8 8 9 9 10 10 11 11 12 12 13 13 14 14 15 15 16 16 17 17 18 18 19 19 20 20 21 21 22 22 23 23 24 24 25 25 26 26 27 27 28 28 29 29 30 30 31 31 32 32 33 33 34 34 35 35 36 36 37 37 38 38 39 39 40 40 41 41 42 42 43 43 44 44 45 45 46 46 47 47 48 48 49 49 50 50 51 51 52 52 53 53 54 54 55 55 56 56 57 57 58 58 59 59 60 60 61 61 Definition 2. An m-coloring of the (n,k)-Kneser graph is a map cfrom n kto [m], such that for S,T∈n k, if S∩T= ∅, then c(S)6= c(T). If ℓ∈ [m], then the color class Pℓis the set of vertices assigned the color ℓby c. The formulas Knesern kare the natural propositional translations of the statement that there is no (n−2k+1)-coloring of the (n,k)-Kneser graph: Definition 3. Let n≥2k>1, and m=n−2k+1. For S∈n kand i∈ [m], the propositional variable pS,ihas the intended meaning that vertex Sof the Kneser graph is assigned the color i. The formula Knesern kis ^ S∈n k_ i∈[m] pS,i→_ S,T∈n k S∩T=∅ _ i∈[m]pS,i∧pT,i. Theorem 4. For fixed parameter k≥1, the propositional translations Knesern kof the Kneser–Lovász theorem have polynomial size extended Frege proofs. Theorem 5. For fixed parameter k≥1, the propositional translations Knesern kof the Kneser–Lovász theorem have quasi-polynomial size Frege proofs. When both kand nare allowed to vary, it is open whether the Knesern ktautologies have quasi-polynomial size (extended) Frege proofs, or equivalently, have proofs with size quasi-polynomially bounded in terms of nk. 3. Mathematical arguments Section 3.1 gives the new proof of the Kneser–Lovász theorem; this is later shown to be formalizable with polynomial size extended Frege proofs. Section 3.2 gives a slightly more complicated but more efficient proof, later shown to be formalizable with quasi-polynomial size Frege proofs. The next definition and lemma are crucial for Sections 3.1 and 3.2. Any two vertices in a color class Pℓhave nonempty intersection. One way this can happen is for the color class to be “star-shaped”: Definition 6. A color class Pℓis star-shaped if TPℓis nonempty. If Pℓis star-shaped, then any i∈TPℓis called a central node of Pℓ. The intuition is that non-starshaped color classes are too small to cover all n kvertices. The Hilton–Milner theorem [19] (which is a refinement of the Erd˝ os–Ko–Rado [16] theorem on intersecting families of finite sets, and improves on Theorem 2(ii) of [16]) implies that if a color class Pℓis not star-shaped then Pℓhas size |Pℓ| ≤ 1+n−1 k−1−n−k−1 k−1. A simpler proof of their bound was given by Frankl and Füredi [17]. Hilton and Milner also observe that their bound is optimal. Instead of using the Hilton–Milner bound, we state a weakened form as Lemma 7, which has a substantially simpler proof. (By comparison, the Hilton–Milner bound is ≤kn−2 k−2for k≥3.) Lemma 7 will be used in our proof of the Kneser–Lovász theorem to establish the existence of star-shaped color classes. Lemma 7. Let cbe a coloring of n k. If Pℓis not star-shaped, then |Pℓ| ≤ k2n−2 k−2. Proof. Suppose Pℓis not star-shaped. If Pℓis empty, the claim is trivial. So suppose Pℓ6= ∅, and let S0= {a1, . . . ,ak}be some element of Pℓ. Since Pℓis not star-shaped, there must be sets S1, . . . , Sk∈Pℓwith ai/∈Sifor i=1, . . . ,k. To specify an arbitrary element Sof Pℓ, we do the following. Since Sand S0have the same color, S∩S0is nonempty. We first specify some ai∈S∩S0. Likewise, S∩Siis nonempty; we second specify some b∈S∩Si. By construction, ai6= b, so Sis fully specified by the kpossible values for ai, the kpossible values for b, and the n−2 k−2possible values for the remaining members of S. Therefore, |Pℓ| ≤ k2n−2 k−2.✷ 3.1. Argument for extended Frege proofs Let k>1 be fixed. We prove the Kneser–Lovász theorem by induction on n. The base cases for the induction are n= 2k, . . . , N(k)where N(k)is the constant depending on kspecified in Lemma 8. We shall show that N(k)is no greater than k4. Since kis fixed, there are only finitely many base cases. Since the Kneser–Lovász theorem is true, these base cases can all be proved by a fixed Frege proof of finite size (depending on k). Therefore, in our proof below, we only show the induction step. ARTICLE IN PRESS UNCORRECTED PROOF Please cite this article in press as: J. Aisenberg et al., Short proofs of the Kneser–Lovász coloring principle, Inf. Comput. (2018), https://doi.org/10.1016/j.ic.2018.02.010 JID:YINCO AID:4352 /FLA [m3G; v1.230; Prn:8/02/2018; 13:15] P.5 (1-15) J. Aisenberg et al. / Information and Computation ••• (••••)•••–••• 5 1 1 2 2 3 3 4 4 5 5 6 6 7 7 8 8 9 9 10 10 11 11 12 12 13 13 14 14 15 15 16 16 17 17 18 18 19 19 20 20 21 21 22 22 23 23 24 24 25 25 26 26 27 27 28 28 29 29 30 30 31 31 32 32 33 33 34 34 35 35 36 36 37 37 38 38 39 39 40 40 41 41 42 42 43 43 44 44 45 45 46 46 47 47 48 48 49 49 50 50 51 51 52 52 53 53 54 54 55 55 56 56 57 57 58 58 59 59 60 60 61 61 Lemma 8. Fix k>1. There is an N(k)so that, for n>N(k), any (n−2k+1)-coloring of n khas at least one star-shaped color class. Proof. Suppose that a coloring chas no star-shaped color class. Since there are n−2k+1 many color classes, Lemma 7 implies that (n−2k+1)·k2n−2 k−2≥n k.(1) For fixed k, the left-hand side of (1) is 2(nk−1)and the right-hand side is 2(nk). Thus, there exists an N(k)such that (1) fails for all n>N(k). Hence for n>N(k), there must be at least one star-shaped color class. ✷ To obtain an upper bound on the value of N(k), note that (1) is equivalent to (n−2k+1)k3(k−1)≥n(n−1). (2) Since 2k−1≥1, (2) implies that (n−1)k4>n(n−1)and thus that n<k4. Thus, (1) will be false if n≥k4; so N(k) < k4. We are now ready to give our first proof of the Kneser–Lovász theorem. Proof of Theorem 1, except for base cases. Fix k>1. By Lemma 8, there is some N(k)such that for n>N(k), any (n−2k+1)-coloring cof n khas a star-shaped color class. As discussed above, the cases where n≤N(k)are handled by exhaustive search and the truth of the Kneser–Lovász theorem. For n>N(k), we prove Theorem 1 by infinite descent. In other words, we show that if cis an (n−2k+1)-coloring of n k, then there is some c′that is an ((n−1)−2k+1)-coloring of n−1 k. By Lemma 8, the coloring chas some star-shaped color class Pℓwith central node i. Without loss of generality, i=n and ℓ=n−2k+1. Let c′=c↾n−1 k be the restriction of cto the domain n−1 k. This discards the central node nof Pℓ, and thus all vertices with color ℓ. Therefore, c′is an ((n−1)−2k+1)-coloring of n−1 k. This completes the proof. ✷ 3.2. Argument for Frege proofs We now give a second proof of the Kneser–Lovász theorem. The proof above required n−N(k)rounds of infinite descent to transform a Kneser graph on nnodes to one on N(k)nodes. Our second proof replaces this with only O(logn)many rounds, and this efficiency will be key for formalizing this proof with quasi-polynomial size Frege proofs in Section 4.2. We refine Lemma 8 to show that for nsufficiently large, there are many (i.e., a constant fraction) star-shaped color classes. The idea is to combine the upper bound of Lemma 7 on the size of non-starshaped color classes with the trivial upper bound of n−1 k−1on the size of star-shaped color classes. Lemma 9. Fix k>1and 0< β < 1. Then there exists an N(k, β) such that for n>N(k, β), if cis an (n−2k+1)-coloring of n k, then chas at least n kβmany star-shaped color classes. Proof. The value of N(k, β) can be set equal to k3(k−β) 1−β. Let n>k3(k−β) 1−β, and suppose cis an (n−2k+1)-coloring of n k. Let αbe the number of star-shaped color classes of c. It is clear that an upper bound on the size of each star-shaped color class is n−1 k−1. There are n−α−2k+1 many non-starshaped classes, and Lemma 7 bounds their size by k2n−2 k−2. This implies that n−1 k−1α+k2n−2 k−2(n−α−2k+1)≥n k.(3) Assume for a contradiction that α<n kβ. Since n>k3(k−β) 1−β, 0 < β < 1, and k≥2, we have n−1>k3(k−1) > k2(k−1). Therefore, n−1 k−1>k2n−2 k−2, and if αis replaced by the larger value n kβ, the left hand side of (3) increases. Thus, n−1 k−1n kβ+k2n−2 k−2n−n kβ−2k+1>n k. Since n−1 k−1n k=n kand n−n kβ−2k+1=k−β kn−2k+1, k2n−2 k−2k−β kn−2k+1> (1−β)n k. ARTICLE IN PRESS UNCORRECTED PROOF Please cite this article in press as: J. Aisenberg et al., Short proofs of the Kneser–Lovász coloring principle, Inf. Comput. (2018), https://doi.org/10.1016/j.ic.2018.02.010 JID:YINCO AID:4352 /FLA [m3G; v1.230; Prn:8/02/2018; 13:15] P.6 (1-15) 6J. Aisenberg et al. / Information and Computation ••• (••••)•••–••• 1 1 2 2 3 3 4 4 5 5 6 6 7 7 8 8 9 9 10 10 11 11 12 12 13 13 14 14 15 15 16 16 17 17 18 18 19 19 20 20 21 21 22 22 23 23 24 24 25 25 26 26 27 27 28 28 29 29 30 30 31 31 32 32 33 33 34 34 35 35 36 36 37 37 38 38 39 39 40 40 41 41 42 42 43 43 44 44 45 45 46 46 47 47 48 48 49 49 50 50 51 51 52 52 53 53 54 54 55 55 56 56 57 57 58 58 59 59 60 60 61 61 Expanding the binomial coefficients yields k3(k−1)k−β kn−2k+1> (1−β)n(n−1). We have k−β k(n−1) > k−β kn−2k+1. Therefore, k3(k−1)k−β k(n−1) > (1−β)n(n−1). Dividing by n−1 gives k3(k−β) > (1−β)n, contradicting n>k3(k−β) 1−β.✷ We now give our second proof of the Kneser–Lovász theorem. Proof of Theorem 1, except for base cases. Fix k>1. By Lemma 9 with β=1/2, if n>N(k,1/2)and cis an (n−2k+1)- coloring of n k, then chas at least n/2kmany star-shaped color classes. We prove the Kneser–Lovász theorem by induction on n. The base cases are where 2k≤n≤N(k,1/2), and there are only finitely of these, so they can be exhaustively proven. For n>N(k,1/2), we structure the induction proof as an infinite descent. In other words, we show that if cis an (n−2k+1)-coloring of n k, then there is some c′that is an ((n−n 2k)−2k+1)-coloring of n−n 2k k. For simplicity of notation, we assume n 2kis an integer. If this is not the case, we really mean to round up to the nearest integer ⌈n 2k⌉. By permuting the color classes and the nodes, we can assume w.l.o.g. that the n 2kcolor classes Pℓfor ℓ=n−n 2k− 2k+2, . . . ,n−2k+1 are star-shaped, and each such Pℓhas a central node in {n−(n/2k)+1, . . . ,n}. That is, the last n 2k many color classes are star-shaped, and they all have a central node among the last n 2knodes in [n]. We shall discard these n/2kmany star-shaped color classes, and the topmost n/2kmany nodes. This discards the central nodes of the discarded color classes, thereby removing all the vertices of the Kneser graph which are assigned discarded color classes. (It is possible that some star-shaped color classes share central nodes. We only need to be sure to discard at least one central node for each color classes, and thus, in this case, additional nodes can be discarded so that n/2kare discarded in all.) More formally, define c′to be the coloring of n−n/2k kwhich assigns the same colors as c. The map c′is a (2k−1 2kn− 2k+1)-coloring of 2k−1 2kn k, since n−n 2k=2k−1 2kn. This completes the proof of the induction step. ✷ When formalizing the above argument with quasi-polynomial size Frege proofs, it will be important to know how many iterations of the procedure are required to reach the base cases, so let us calculate this. After siterations of this procedure, we have a (( 2k−1 2k)sn−2k+1)-coloring of (2k−1 2k)sn k. We pick slarge enough so that (2k−1 2k)snis less than N(k,1/2). In other words, since kis constant, s=log 2k 2k−1n k3(2k−1)=O(logn) will suffice, and only O(logn)many rounds of the procedure are required. 3.3. Optimal colorings of Kneser graphs This section is a brief diversion motivated by the question of whether Lemma 9 about the number of non-starshaped colors is optimal. It is well-known that n khas an (n−2k+2)-coloring [25]. A simple construction of such a coloring, which we call c1, is given here for completeness as follows. For S∈n k, define c1(S)by: (1) If S*[2k−1], let c1(S)=max(S)−(2k−2). Clearly 1 <c1(S)≤n−2k+2. (2) If S⊆ [2k−1], let c1(S)=1. We claim that c1defines a proper coloring. By construction, if c1(S) > 1, then c1(S)+(2k−2)∈S. Thus, if c1(S)=c1(S′) > 1, then S∩S′6= ∅ and Sand S′are not joined by an edge in the Kneser graph. On the other hand, if c1(S)=1, then Scontains kelements from the set [2k−1]. Any two such subsets have nonempty intersection, and therefore if c1(S)=c1(S′)=1, then again S∩S′6= ∅. Note that c1contains n−2k+1 many star-shaped color classes, and only one non-starshaped color class. In view of Lemma 9, it is interesting to ask whether it is possible to give (n−2k+2)-colorings which have fewer star-shaped color classes and more non-starshaped color classes. The next theorem gives the best construction we know. Theorem 10. Let k≥1and n≥3k−3. There is an (n−2k+2)coloring ck−1of n kwhich has k−1many non-starshaped color classes and only n−3k+3many star-shaped color classes. ARTICLE IN PRESS UNCORRECTED PROOF Please cite this article in press as: J. Aisenberg et al., Short proofs of the Kneser–Lovász coloring principle, Inf. Comput. (2018), https://doi.org/10.1016/j.ic.2018.02.010 JID:YINCO AID:4352 /FLA [m3G; v1.230; Prn:8/02/2018; 13:15] P.7 (1-15) J. Aisenberg et al. / Information and Computation ••• (••••)•••–••• 7 1 1 2 2 3 3 4 4 5 5 6 6 7 7 8 8 9 9 10 10 11 11 12 12 13 13 14 14 15 15 16 16 17 17 18 18 19 19 20 20 21 21 22 22 23 23 24 24 25 25 26 26 27 27 28 28 29 29 30 30 31 31 32 32 33 33 34 34 35 35 36 36 37 37 38 38 39 39 40 40 41 41 42 42 43 43 44 44 45 45 46 46 47 47 48 48 49 49 50 50 51 51 52 52 53 53 54 54 55 55 56 56 57 57 58 58 59 59 60 60 61 61 Proof. To construct ck−1, partition the set [n]into n−2k+2 many subsets T1, . . . , Tn−2k+2as follows. For i≤n−3k+3, Tiis chosen to be a singleton set, say Ti= {n−i+1}. The remaining k−1 many Ti’s are subsets of size 3, say Ti= { j−2,j−1,j} where j=3(i−(n−3k+3)). Since n=(n−3k+3)+3(k−1), the sets Tipartition [n], and each Tihas cardinality either 1 or 3. For Sa subset of nof cardinality k, define the color ck−1(S)to equal the least isuch that |S∩Ti|>1 2|Ti|. We claim there must exist such an i. If not, then Scontains no members of the singleton subsets Tiand at most one member of each of the subsets Tiof size three. But there are only k−1 many subsets of size three, contradicting |S| = k. It is easy to check that if ck−1(S)=ck−1(S′)then S∩S′6= ∅. Thus ck−1is a coloring. Furthermore, ck−1has k−1 many non-starshaped color classes and n−3k+3 many star-shaped color classes. ✷ Theorem 10 can be extended to show that when 2k≤n≤3k−3, there is a n−2k+2 coloring with no star-shaped color class. The proof construction uses a similar idea, based on the fact that [n]can be partitioned into n−2k+2≤k−1 many subsets, each of odd cardinality ≥3. We leave the details to the reader. Question 11. Do there exist (n−2k+2)-colorings of the (n,k)-Kneser graphs with more than k−1 many non-starshaped color classes? 4. Formalization in propositional logic 4.1. Polynomial size extended Frege proofs We sketch the formalization of the argument in Section 3.1 as a polynomial size extended Frege proof, establishing Theorem 4. We concentrate on showing how to express concepts such as “star-shaped color class” with polynomial size propositional formulas. For expository reasons, we omit the straightforward details of how (extended) Frege proofs can prove properties of these concepts. Fix values for kand nwith n>N(k). We describe an extended Frege proof of Knesern k. We have variables pS,j(recall Definition 3), collectively denoted E p. The proof assumes Knesern k(E p)is false, and proceeds by contradiction. The main step is to define new variables E p′with the extension rule and prove that Knesern−1 k(E p′)fails. This will be repeated until reaching a Kneser graph over only N(k)nodes. For this, let Star(i, ℓ) express that i∈ [n]is a central node of the color class Pℓ; namely, Star(i, ℓ) := ^ S∈n k,i/∈S ¬pS,ℓ. Note that Pℓmay have more than one central node. Conversely, a node imay be a central node for more than one color class. We use Star(ℓ) := WiStar(i, ℓ) to express that Pℓis star-shaped. The extended Frege proof defines an instance of the Kneser–Lovász principle Knesern−1 kby discarding one node and one color. The first star-shaped color class Pℓis discarded; accordingly, we let DiscardColor(ℓ) := Star(ℓ) ∧^ ℓ′<ℓ ¬Star(ℓ′). The node to be discarded is the least central node of the discarded Pℓ: DiscardNode(i):= _ ℓhDiscardColor(ℓ) ∧Star(i, ℓ) ∧^ i′<i ¬Star(i′, ℓ)i. After discarding the node iand the color ℓ, the remaining nodes and colors are renumbered to the ranges [n−1]and [n−2k], respectively. In particular, the “new” color j(in the instance of Knesern−1 k) corresponds to the “old” color j−ℓ(in the instance of Knesern k) where j−ℓ=(jif j< ℓ j+1 if j≥ℓ. And, if S= {i1, . . . , ik} ∈ n−1 kis a “new” vertex (for the Knesern−1 kinstance), then it corresponds to the “old” vertex S−i∈n k (for the instance of Knesern k), where S−i= {i′ 1,i′ 2, . . . , i′ k}with ARTICLE IN PRESS UNCORRECTED PROOF Please cite this article in press as: J. Aisenberg et al., Short proofs of the Kneser–Lovász coloring principle, Inf. Comput. (2018), https://doi.org/10.1016/j.ic.2018.02.010 JID:YINCO AID:4352 /FLA [m3G; v1.230; Prn:8/02/2018; 13:15] P.8 (1-15) 8J. Aisenberg et al. / Information and Computation ••• (••••)•••–••• 1 1 2 2 3 3 4 4 5 5 6 6 7 7 8 8 9 9 10 10 11 11 12 12 13 13 14 14 15 15 16 16 17 17 18 18 19 19 20 20 21 21 22 22 23 23 24 24 25 25 26 26 27 27 28 28 29 29 30 30 31 31 32 32 33 33 34 34 35 35 36 36 37 37 38 38 39 39 40 40 41 41 42 42 43 43 44 44 45 45 46 46 47 47 48 48 49 49 50 50 51 51 52 52 53 53 54 54 55 55 56 56 57 57 58 58 59 59 60 60 61 61 i′ t=(itif it<i it+1 if it≥i. For each S∈n−1 kand j∈ [n−2k], the extended Frege proof uses the extension rule to introduce a new variable p′ S,j defined as follows p′ S,j≡_ i,ℓ DiscardNode(i)∧DiscardColor(ℓ) ∧pS−i,j−ℓ. As seen in the definition by extension, p′ S,jis defined by cases, one for each possible pair i, ℓ of nodes and colors such that the node iis the least central node of the Pℓcolor class, where Pℓis the first star-shaped color class. The extended Frege proof then shows that ¬Knesern k(E p)implies ¬Knesern−1 k(E p′), i.e., that if the variables pS,jdefine a coloring, then the variables p′ S,jalso define a coloring. The first step for the extended Frege proof is to show that there is at least one star-shaped color class, and then there is a unique ℓsuch that DiscardColor(ℓ) holds. In fact, we claim there are polynomial size Frege proofs of _ ℓ DiscardColor(ℓ) (4) and ^ ℓ1<ℓ2 (¬DiscardColor(ℓ1)∨ ¬DiscardColor(ℓ2)).(5) The Frege proof of (4) and (5) starts by proving WℓStar(ℓ). This is done essentially via a proof by contradiction: First, under the hypothesis that ¬WℓStar(ℓ), the Frege proof uses the argument of Lemma 7 to show, for each color class Pℓ, that there is a surjective map πℓfrom [k2n−2 k−2]onto Pℓ. Fixing a particular value for ℓ, the Frege proof defines πℓas follows: It chooses a set S0in Pℓ, say the lexicographically first set S0in Pℓ. There are ≤n kmany possible choices for this S0; and the Frege proof splits into cases based on S0. Then, letting S0= {a1, . . . ,ak}in increasing order, the Frege proof proves, for each i the existence of a lexicographically first set Siin Pℓwith ai/∈Si(using the assumption that Pℓis not star-shaped). The Frege proof further splits into polynomially many cases for all possible choices of S1, . . . , Sk. Let ai,i′be the i′-th member of Si. For each j6= j′∈ [n], there is a natural bijection πj,j′from n−2 k−2to the (k−2)-subsets of [n] \ { j,j′}. For i,i′∈ [k] and p∈n−2 k−2, the surjection πℓcan be defined by π(i,i′,p)= {ai,ai,i′,πai,ai,i′(p)}if this a well-defined member of Pℓ, and π(i,i′,p)=S0otherwise. The intersection properties of Pℓ, as in the proof of Lemma 7, show immediately that πℓis surjective. Using the formalization of “counting” in Frege proofs [9], the surjectivity of πℓimplies that |Pℓ| ≤ k2n−2 k−2. But since (n−2k+1)k2n−2 k−2<n k, this contradicts the fact that every vertex is in a color class. The fact that (n−2k+1)k2n−2 k−2<n k is proved by just computing the values of both sides of the inequality. Indeed, kis fixed, so there are only n k<nkmany vertices, and we are only counting polynomially many vertices. Once WℓStar(ℓ) has been proved with a polynomial size proof (under the hypothesis that ¬Knesern k(E p)), the formulas (4) and (5) follow easily. Likewise, there are polynomial size Frege proofs that there is a unique value i∈ [n−2k+1]which satisfies DiscardNode(i). For fixed values of ℓand i, a polynomial size Frege proof now establishes DiscardColor(ℓ) ∧DiscardNode(i)∧Knesern−1 k(E p′)→Knesern k(E p). This Frege proof argues as follows, assuming DiscardColor(ℓ) and DiscardNode(i)and Knesern−1 k(E p′). Since Knesern−1 k(E p′)is true, either (a) its hypothesis is false and we have Vn−2k j=1¬p′ S,jfor some S∈n kor (b) its conclusion is true and there are S,T∈n kand jsuch that S∩T= ∅ and p′ S,jand p′ T,j. If (a) holds then ¬pS−i,j−ℓfor all j∈ [n−2k]and this together with the fact that i/∈S−iand iand ℓwere discarded further implies that the hypothesis of Knesern k(E p)is false so Knesern k(E p)is true. Likewise, if (b) holds, then using S−iand T−iand j−ℓshows that the conclusion of Knesern kis true. Putting all these arguments together gives the desired Frege proof of ¬Knesern k(E p)→ ¬Knesern−1 k(E p′). The extended Frege proof iterates this process of removing one node and one color until it is shown that there is a coloring of N(k) k. This is then refuted by exhaustively considering all colorings of Kneser graphs on ≤N(k)nodes. ✷ ARTICLE IN PRESS UNCORRECTED PROOF Please cite this article in press as: J. Aisenberg et al., Short proofs of the Kneser–Lovász coloring principle, Inf. Comput. (2018), https://doi.org/10.1016/j.ic.2018.02.010 JID:YINCO AID:4352 /FLA [m3G; v1.230; Prn:8/02/2018; 13:15] P.9 (1-15) J. Aisenberg et al. / Information and Computation ••• (••••)•••–••• 9 1 1 2 2 3 3 4 4 5 5 6 6 7 7 8 8 9 9 10 10 11 11 12 12 13 13 14 14 15 15 16 16 17 17 18 18 19 19 20 20 21 21 22 22 23 23 24 24 25 25 26 26 27 27 28 28 29 29 30 30 31 31 32 32 33 33 34 34 35 35 36 36 37 37 38 38 39 39 40 40 41 41 42 42 43 43 44 44 45 45 46 46 47 47 48 48 49 49 50 50 51 51 52 52 53 53 54 54 55 55 56 56 57 57 58 58 59 59 60 60 61 61 4.2. Quasi-polynomial size Frege proofs This section discusses some of the details of the formalization of the argument in Section 3.2 as quasi-polynomial size Frege proofs, establishing Theorem 5. First we will form an extended Frege proof, then modify it to become a Frege proof. As before, the proof starts with the assumption that Knesern k(E p)is false. As we describe next, the extended Frege proof then introduces variables E p′by extension so that Knesern−n/2k k(E p′)is false. This process will be repeated O(logn)times. The final Frege proof is obtained by unwinding the definitions by extension. For a set Xof formulas and t>0, we now use the notation “|X| ≤ t” to denote a formula that is true when the number of true formulas in Xis less than or equal to t. As already discussed, “|X| ≤ t” can be expressed by a formula of size polynomially bounded by the total size of the formulas in X, using the construction in [9]. “|X| = t” is defined similarly. The formulas Star(i, ℓ) and Star(ℓ) are the same as in Section 4.1. A color ℓis now discarded if it is among the least n/2k star-shaped color classes. DiscardColor(ℓ) := Star(ℓ) ∧|{Star(ℓ′):ℓ′≤ℓ}| ≤ n/2k The discarded nodes are the least central nodes of the discarded color classes. DiscardNode(i):= _ ℓhDiscardColor(ℓ) ∧Star(i, ℓ) ∧^ i′<i ¬Star(i′, ℓ)i. DiscardNode(i)will hold for at most n/2kmany nodes i, since there are only n/2kmany discarded colors. We could modify the definition of DiscardNode to discard exactly n/2kmany nodes; however, this is not strictly necessary, as the only use of DiscardNode is to define the predicate RenumNode(i′,i)below, and that definition effectively discards exactly n/2kmany nodes even if DiscardNode(i)picks out fewer than n/2kmany nodes to be discarded. The remaining, non-discarded colors and nodes are renumbered to form an instance of Knesern−n/2k k. For this, the formula RenumNode(i′,i)is true when the node i′is the i-th node that is not discarded; similarly RenumColor(j′,j)is true when the color j′is the j-th color that is not discarded. RenumNode(i′,i):= |{¬DiscardNode(i′′):i′′≤i′}| = i∧ ¬DiscardNode(i′) RenumColor(j′,j):= |{¬DiscardColor(j′′):j′′≤j′}| = j∧ ¬DiscardColor(j′) The predicate RenumNode(i′,i)defines a bijection between the sets [n−n/2k]and the non-discarded nodes of [n]. Likewise, the predicate RenumColor(j′,j)defines a bijection between [(n−n/2k)−2k+1]and the non-discarded colors. For each S= {i1, . . . , ik} ∈ n−n/2k kand j∈ [(n−n/2k)−2k+1], we define by extension p′ S,j≡_ i′ 1,...i′ k,j′ k ^ t=1RenumNode(i′ t,it)∧RenumColor(j′,j)∧p{i′ 1,...,i′ k},j′!. The Frege proof then argues that if the variables pS,jdefine a coloring, then the variables p′ S,jdefine a coloring, i.e., that ¬Knesern k(E p)→ ¬Knesern−n/2k k(E p′). The first step for this is proving that there are at least n/2kstar-shaped color classes by formalizing the proofs of Lemmas 7 and 9. Those proofs were “counting” arguments: they involved counting the number of members of n kthat are contained in the color classes Pℓ. As already mentioned, the proof of Lemma 7 can be formalized with polynomial size Frege proofs proving that, if Pℓis a non-starshaped color class, there is a surjective map from [k2n−2 k−2]onto Pℓand from this concluding that |Pℓ| ≤ k2n−2 k−2. Similarly, and even easier, there are polynomial size Frege proofs of the fact that if Pℓis star-shaped, then there is a surjective map from n−1 k−1onto Pℓ, from whence |Pℓ| ≤ n−1 k−1. The Frege proof then splits into polynomially many cases depending on the number αof star-shaped color classes. For each α, the inequality (3) must hold by the upper bounds on the |Pℓ|’s. However, for any fixed value of α<n kβ=n 2k, directly substituting the (fixed) values of n,k,αinto (3) shows that it is false.6It follows that α≥n 2k; that is, there are ≥n 2kmany star-shaped colors. From this, it follows, again with a polynomial size Frege proof, that RenumNode(i′,i)and RenumColor(j′,j)define bijections. After that, it is straightforward to prove that, for each S∈n−n/2k kand j∈ [(n−n/2k)−2k+1], the variable p′ S,jis well-defined. In addition, a polynomial size Frege proof can prove that if Knesern k(E p)is false, then Knesern−n/2k k(E p′)is false. This is iterated O(logn)times until fewer than N(k,1/2)nodes remain. The proof concludes with a hard-coded proof that there are no such colorings of the finitely many small Kneser graphs. To form the quasi-polynomial size Frege proof, we unwind the definitions by extension. Each definition by extension was polynomial size; they are nested to a depth of O(logn). So the resulting Frege proof is quasi-polynomial size. ✷ 6We know that (3) is false by the argument given in the proof of Lemma 9; therefore a Frege proof can use direct calculation to verify this for the needed values of n,k,α. Alternatively, a polynomial size Frege proof can carry out all the steps of the argument used earlier to establish (3); however, this is not necessary, and does not seem to add anything apart from possibly a bit more uniformity. ARTICLE IN PRESS UNCORRECTED PROOF Please cite this article in press as: J. Aisenberg et al., Short proofs of the Kneser–Lovász coloring principle, Inf. Comput. (2018), https://doi.org/10.1016/j.ic.2018.02.010 JID:YINCO AID:4352 /FLA [m3G; v1.230; Prn:8/02/2018; 13:15] P.16 (1-15) 1 1 2 2 3 3 4 4 5 5 6 6 7 7 8 8 9 9 10 10 11 11 12 12 13 13 14 14 15 15 16 16 17 17 18 18 19 19 20 20 21 21 22 22 23 23 24 24 25 25 26 26 27 27 28 28 29 29 30 30 31 31 32 32 33 33 34 34 35 35 36 36 37 37 38 38 39 39 40 40 41 41 42 42 43 43 44 44 45 45 46 46 47 47 48 48 49 49 50 50 51 51 52 52 53 53 54 54 55 55 56 56 57 57 58 58 59 59 60 60 61 61 Sponsor names Do not correct this page. Please mark corrections to sponsor names and grant numbers in the main text. NSF,country=United States, grants=DMS-1101228, CCF-1213151 Simons Foundation,country=United States, grants=306202