The Earth–Moon problem: a certified corpus of nine-critical biplanar graphs, the exhaustion of the known χ = 10 candidates, and the status of χ₂

We report a complete computational and formal campaign on Ringel's Earth–Moon problem, which asks for the maximum chromatic number χ₂ of graphs of thickness two (9 ≤ χ₂ ≤ 12). We certify a corpus of 241 biplanar graphs: the full 40-graph Boutin–Gethner–Sulanke catalogue (recovered from the paper's figures and SAT-verified), together with over 30 new nine-critical biplanar graphs obtained by Hajós sums and edge-swap search, each with explicit planar layer witnesses and SAT-certified chromatic number and criticality. On the exclusion side we give complete proofs that every known 10-chromatic candidate is non-biplanar: CAND-P = C₅(4,4,4,4,3) (19v/99e) — the graph first shown non-biplanar by Kirchweger–Scheucher–Szeider (SAT 2023) via 12 hours of SAT-modulo-symmetries — which we re-prove by a four-line triangle-free counting argument; K₃+D₇ (16v/83e) by K₉-containment (θ(K₉)=3); and CAND-A (22v/120e) by a bridge-edge obstruction at the maximal-planar boundary. We further identify a new nine-critical graph C₅(3,4,3,4,3) (17 vertices, 78 edges, ω=7, fully vertex- and edge-critical by SAT) whose universal apex (18 vertices, 95 edges) is 10-chromatic and sits one edge under the biplanar boundary 6n−12; a completed SAT-modulo-symmetries refutation gives C₅(3,4,3,4,3) thickness exactly 3 [CERTIFIED end-to-end, 2026-08-25], and the apex is then excluded a fortiori. We assemble the sharpest current order ladder: χ₂ ≥ 10 forces n ≥ 14 (Folkman, re-proved in-house both ways), n ≥ 16 for triangulation unions, n ≥ 17 unconditionally — independently confirming Doria (Zenodo, 6 Aug 2026) by a route free of his census dependency — (via the Gallai join theorem: three join cases verified in Lean modulo axiomatised graph-theoretic facts (§8), certified SAT windows at n = 13, 14, and a window collapse driven by the Kostochka–Stiebitz exceptional family, whose members all contain Kh−1), and n ≥ 19 modulo exactly five remaining SAT values — e ∈ {58,59} on 15 vertices and e ∈ {61,62,63} on 16 — plus one enumeration at 17; the (4,6) and (3,7) join cases are closed exactly. On the upper side we observe that the published Kelly-Postle conjecture on the density of critical graphs with no large cliques implies χ₂ ≤ 11 in one line — the first movement of Ringel's 1959 bound would follow — and that their corresponding theorem already holds for large k, failing at k = 12 only through its "sufficiently large" hypothesis (§7.2). We formalize in Lean the lower bound χ₂ ≥ 9 and the degeneracy machinery behind the upper bound χ₂ ≤ 12. The known χ=10 candidate space is exhausted — including both named candidates of Gethner's 2018 survey: C₅⊠K₄−v (= our CAND-P) and C₇⊠K₄, the latter untested by any prior work and killed here by a four-line counting argument that disposes of the entire family C_m⊠K_t (m ≥ 5, t ≥ 4) — with the apex of C₅(3,4,3,4,3) included, its exclusion now certified end-to-end (both SMS refutations passed drat-trim with zero RAT lemmas, §9); the certified exclusions remove every χ = 10 candidate the literature has named. We read this as evidence for χ₂ = 9 rather than support for it: it bounds the candidates that have been written down, not the space they were drawn from. We also correct several campaign records — most importantly the false "e > 5n−6 for every nine-critical biplanar graph" conjecture, which is refuted by the Hajós sum of two copies of Sulanke's graph (21 vertices, 99 = 5·21−6 edges).