Biplanar graphs with independence number two are 9-colorable

1 Introduction

• Sulanke’s graph establishes a 9-color lower bound, while 12 colors always suffice, leaving the largest biplanar chromatic number in {9, 10, 11, 12}.Gethner conjectures that the maximum is 11.Source: §1 · p. 1
• For independence number 2, χ(G) ≥ ⌈n/2⌉, so a 19-vertex example would require at least 10 colors and answer Gethner and Sulanke’s question.Their question was to find a thickness-two graph on 19 vertices with triangle-free complement.Source: §1 · p. 1
• A direct 19-vertex search is out of reach, so the proof reduces the problem to 3271 candidate complements and refutes each candidate.The reduction uses the complement of a union of two sphere triangulations and certifies that the candidate list is complete.Source: §1 · p. 2
• Every biplanar graph with independence number at most 2 is 9-colorable, and none on 19 vertices has independence number at most 2.The latter answers the 19-vertex question posed by Gethner and Sulanke.Source: §1 · p. 2
• For orders at most 18, a matching argument reduces a minimal counterexample to an 18-vertex graph with a universal vertex, which Lemma 3 excludes.Theorem 2 excludes order 19; Lemma 3 rules out the remaining reduced case.Source: §1 · p. 2
• Lean 4 checks the computational proofs and the arithmetic in the short reduction to Theorem 1, with three classical planar-graph facts assumed.The SAT refutations are checked in Lean, and the development and certificates are available on Zenodo.Source: §1 · pp. 2–3

2 The reduction

• A graph has independence number at most 2 exactly when its complement is triangle-free; biplanarity can be treated as equality with the union of two planar layers using (X1).The proof assumes three classical planar-graph facts, including completion of a planar graph to a sphere triangulation and that K9 is not biplanar; planarity itself is not formalized.Source: §2 · p. 3
• The proof uses sphere triangulations as combinatorial objects; the stated conditions force a sphere, but a triangle in one need not be a face.A triangle may be a separating triangle, as illustrated in Figure 1.Source: §2 · p. 3, Figure 1 · p. 4
• Every biplanar graph with independence number at most 2 can be enlarged on the same vertices to a union of two sphere triangulations without increasing its independence number.Each planar layer is completed by adding edges; adding edges does not increase independence number.Source: §2 · pp. 3–4
• For a 19-vertex exact union, its complement must be triangle-free, have maximum degree at most 8, have no independent set of size 9, and have 69–76 edges.The edge-count lower bound is 69 plus the number of edges shared by the triangulations; the degree bound gives the upper bound 76.Source: §2 · p. 4
• A biplanar graph with independence number at most 2 has at most 19 vertices; in the 18-vertex universal-vertex case, the complement has an isolated vertex and 57–59 edges.In that case every other complement vertex has degree at most 7, and the complement has no independent set of size 9.Source: §2 · p. 4

3 Enumeration of the candidates

• The SAT encoding imposes triangle-freeness, no independent 9-set, degree bounds, and edge-count bounds; enumeration produced 3271 order-19 isomorphism classes and four order-18 candidates.The order-19 run produced 3278 graphs in those classes; the four order-18 graphs are pairwise non-isomorphic.Source: §3 · p. 5
• The order-19 formula F∧S∧B was refuted in 43 minutes, and the corresponding order-18 formula was refuted in 98 seconds.CaDiCaL produced LRAT proofs for both unsatisfiability checks.Source: §3 · p. 5
• Lean certifies that every graph satisfying the filter is isomorphic to a listed candidate by checking the encoding, symmetry-breaking clauses, refutation, and candidate isomorphisms.The SMS propagator is not trusted; the emitted clauses are individually verified, and the completeness argument does not require the found graphs’ minimality.Source: §3 · pp. 5–6

4 The exact-union test

• The formula Φ(U) encodes edge and face membership in two layers, requiring every edge of U in at least one layer and specifying doubled edges and triangulation edge counts.It also breaks layer symmetry by requiring the first edge of U in layer 1.Source: §4 · p. 6
• Local clauses alone may admit models that are not sphere triangulations, so link and connectivity cuts are added lazily when a decoded model violates them.The link cuts enforce a single-cycle vertex link; connectivity cuts rule out disconnected layers.Source: §4 · p. 6
• If the strengthened formula Φ_C(U) is unsatisfiable, then U cannot be an exact union of two sphere triangulations.The soundness argument constructs a satisfying assignment from any such pair of triangulations, including for well-formed cuts.Source: §4 · pp. 6–7
• All 3275 final formulas were unsatisfiable, and Lean checked their streamed LRAT proofs against formulas produced by its encoder.The run took 74 CPU-hours; an independent implementation reproduced the verdicts for the 3271 order-19 candidates.Source: §4 · p. 7

5 The Lean statements

• SphereTriangulation packages a graph with triangular faces, 3n−6 edges, two faces per edge, connected vertex links, and a connected graph.The planarity field supplies the planarity condition separately.Source: §5 · pp. 7–8
• Biplanar is formalized as containment in the edge union of two planar graphs, with planarity facts supplied as hypotheses.Ordinary planarity satisfies these facts by the classical results (X1) to (X3), but that instantiation is not formalized.Source: §5 · pp. 7–8
• Table 1 distinguishes verified material, trusted inputs, and paper argument; the archive provides five checking levels, including rerunning the refutations and adversarial controls.The argument of Section 6 outside partition_arith is on paper.Source: Table 1 · p. 8, §5 · pp. 8–9
• The formal theorem excludes a biplanar graph on 19 vertices with no independent set of size 3; a separate order-18 statement assumes a universal vertex.The paper identifies these as Theorem 2 and Lemma 3, respectively.Source: §5 · p. 8
• The proof depends on 6554 native_decide axioms for the order-19 theorem, recording compiled Boolean checks rather than kernel evaluation.The soundness of the checked Boolean functions is proved, but compiled evaluation is a weaker guarantee than evaluation in Lean's kernel.Source: §5 · p. 8

6 Proof of Theorem 1

• A minimal induced subgraph with chromatic number at least 10 is 10-chromatic, becomes 9-colorable after any vertex deletion, and has order at most 18.Its complement H is triangle-free, and the matching argument uses ν(H)=n−10.Source: §6 · p. 9
• For graphs with independence number at most 2, chromatic number equals vertex count minus the maximum matching size in the complement.Color classes of size two form a matching, and a matching gives a coloring by pairing its endpoints.Source: §6 · p. 9
• Gallai–Edmonds structure makes every component of H factor-critical; the number of isolated vertices and nontrivial components satisfies r+k=20−n≥2, with at most three nontrivial components.Each nontrivial component is triangle-free, factor-critical, and has odd order at least five.Source: §6 · p. 9
• The case analysis combines the clique bound r+2k≤8, component degree bounds, and the biplanar edge bound e(G′)≤6n−12.The sum of component edge upper bounds is compared with L(n), with M determined by r and k.Source: §6 · p. 9
• Only n=18, r=1, k=1, and m₁=17 satisfy L(n)≤M; the resulting universal-vertex case is excluded by Lemma 3, yielding 9-colorability.The order bound then follows for biplanar graphs with independence number at most 2.Source: §6 · p. 9

• The known bounds of 9 and 12 on the largest chromatic number of a biplanar graph remain unchanged, but the independence-number-2 route is closed.Source: §7 · p. 10
• By Corollary 4, a 10-chromatic biplanar graph must have independence number at least 3; Thomassen’s smallest named candidate, C7[K4] on 28 vertices, is not biplanar.Source: §7 · p. 10
• An 18-vertex biplanar graph with independence number 2 would have independence ratio 1/9 < 2/17, and order 18 is the only remaining possibility for such an example.Source: §7 · p. 10
• Whether every biplanar graph has independence number at least cn for some c > 1/12 remains open; the result gives α ≥ 3 for orders at least 19 but does not settle this linear bound [3, Problem 4].Source: §7 · p. 10
• The Lean-checked encoding and certified enumeration can apply to other nonexistence questions when candidates can be enumerated and the property has a sound propositional encoding, though the 28-vertex enumeration may be infeasible.Source: §7 · p. 10