# Highlights

Start here. This is the short version of what the project found, what is
proved versus merely evidenced, and where the live edges are. The full
record is [`data/ledger/LEDGER.md`](data/ledger/LEDGER.md), organised by
category; every claim below carries its finding id (`f0NN`) so you can look
up the argument and its evidence there.

## The problem, and where it stands

The Earth–Moon problem asks for the largest chromatic number of a *biplanar*
graph, one whose edges split into two planar layers on a shared vertex set.
The bounds have been `9 ≤ χ ≤ 12` for decades. The upper bound is Ringel's,
via six-colouring each layer. The lower bound rests on a single graph:
Sulanke's `K6 + C5` (11 vertices, 50 edges, χ = 9), which has stood since
the 1970s.

This project hunted for a biplanar graph with χ ≥ 10.

**It did not find one.** 742 candidates were logged and 717 verified; 699
died on planarity. No witness exists in this repository, and nothing here
should be read as claiming otherwise. What the project produced instead is
a large pile of closures, a few results that appear to be new, and tooling
that decides these questions far faster than brute force.

Two constraints govern everything. A biplanar graph obeys the **Euler
ceiling** `m ≤ 6n − 12`, and a 10-critical graph obeys the **criticality
floor** `m ≥ ⌈9n/2⌉`. Candidates live only in the corridor between them,
which is why so much of the work is counting rather than searching.

## Results that may matter outside this project

**A localized biplanarity bound that kills whole families** (`f045`). In any
biplanar graph, for *every* vertex subset `S`, the induced subgraph obeys
`e(G[S]) ≤ 6|S| − 12`; moreover any triangle-free subgraph spanning `h`
vertices has at most `4h − 8` edges. The second form is the workhorse: it
closed the odd-cycle blowup family outright (`f026`) and killed 979 of 1000
candidates in one sweep (`f047`). It is a hereditary strengthening of the
Euler bound and is cheap to check.

**A published open problem, half answered** (`f070`). Albertson, Boutin and
Gethner, *The Thickness and Chromatic Number of r-Inflated Graphs* (Discrete
Math 310(20):2725–2734, 2010), close with Open Problem 3 asking for the
thickness of inflated cycles. The band bound above settles the lower-bound
half.

**The minimum-degree shortcut is dead** (`f071`). Every 10-critical graph has
minimum degree ≥ 9, and biplanarity is hereditary, so "no biplanar graph has
minimum degree 9" would have settled Earth–Moon at χ = 9 immediately. It is
false: biplanar graphs with minimum degree 9, 10 and 11 all exist and were
constructed in seconds. Strikingly, all of them have χ = 6. No impossibility
proof can route through degeneracy, and Ringel's upper bound cannot be
improved that way.

**Every open region is one extremal question** (`f076`). Writing `Ḡ` for the
complement, a witness with independence number `q` needs `Ḡ` to be
`K_{q+1}`-free, and K9-freeness needs `α(Ḡ) ≤ s`. So every unresolved region
of every attack route is an instance of the Ramsey–Turán quantity
`RT(n, K_{q+1}, s)`, the maximum edges of a `K_{q+1}`-free graph on `n`
vertices with independence at most `s`. A region closes with no graph search
at all whenever `RT < need`. This also explains every observed failure: the
binding constraint was never edge count but independence.

**That quantity turned out to have a name** (`f081`). For `q = 2` it is
Andrásfai's problem, settled in 1964: `ex(n,s) = n² − 4ns + 5s²` for
`s/n ∈ [2/5, 1/2]`, with C5-blowups extremal. That gives exact values such
as `RT(17,K₃,7) = 58` and `RT(19,K₃,8) = 73`, which pin the α=2 search
window completely.

**A one-line bound that closes an entire region** (`f078`). In a
triangle-free graph every neighbourhood is independent, so `Δ ≤ α` and hence
`RT(n,K₃,s) ≤ ⌊ns/2⌋`. That kills the whole α=2 join `t=2` region across
`n = 15..19` without a single search, and it is tight at `RT(19,K₃,6) = 57`.

## The low-order programme

The most directly citable line of work. Kirchweger, Scheucher and Szeider
(SAT 2023) proved every biplanar graph on `n ≤ 13` vertices is 9-colourable.
This project closed the next sizes by showing no 10-critical core exists on
them:

| n | finding | how |
|---:|---|---|
| 13 | `f051` | exhaustive enumeration of subcubic complements; max edges 10 < 12 required |
| 14 | `f054` | matching-number case split plus CEGAR; max edges 17 < 19 required |
| 15 | `f052` | Gallai join-decomposition, 11 cases, all forced over the corridor ceiling |
| 17 | `f055` | clique-kill chain forces the complement triangle-free, then dies analytically at 45 < 46 |
| 18 | `f060` | the three concrete candidates closed (specific graphs, **not** the whole regime) |

**n = 16 is in progress** (`f084`, `f086`, `f087`). It is the only gap below
18. Savings dominate the matching number, so Gallai–Edmonds plus Berge–Tutte
splits it into 14 component profiles; the join decomposition then kills 8 of
them by counting alone, in under a second with no solver. Six remain, all of
the shape "one big component plus isolated vertices". The hardest reduces to
a single question about 13 vertices, and Kostochka–Yancey's non-Ore bound
pins its edge count exactly. Closing all six would extend the published
result from `n ≤ 13` to `n ≤ 17`.

## Techniques worth stealing

**The Euler-tight encoding.** When a candidate sits exactly at `m = 6n − 12`,
both layers are forced to be triangulations. Adding per-vertex layer-degree
bounds, per-edge triangle support, monochromatic `K5`/`K3,3` bans and Euler
counting windows makes the seed CNF propositionally UNSAT at round zero, with
no Kuratowski refinement needed at all (`f036`). This is why thousands of
Euler-tight candidates decide in seconds each.

**CEGAR for biplanarity.** One variable per edge, seeded with
no-monochromatic-`K5`/`K3,3` clauses, with Kuratowski subdivisions added
lazily as cuts. See `runs/cegar.py`, independently re-implemented for
cross-checking in `runs/recheck_cegar.py`.

**Complete encodings beat refinement loops when the clause set is small.**
For "clique cover number ≥ 7 on 13 vertices", the lazy loop stalled after
89,000 cuts; the full clause set is one short clause per partition into 6
blocks, and `S(13,6) = 9,321,312` is entirely postable. Streaming clauses
straight into the solver keeps the memory cost in the solver rather than in
Python.

## The verification discipline

Most results here are negative, so the standard of proof is whatever makes an
UNSAT trustworthy. Four rules carry that weight.

**Every decider is validated against a known-satisfiable control** sharing its
exact code path. An over-constrained encoding yields a fast, confident, wrong
UNSAT, and the only reliable detector is a positive control: if the encoding
cannot re-find a graph that provably exists, its UNSAT means nothing. Each
decider ships with one. The biplanarity encodings are validated on
`double_tri_19`, a doubled triangulation that is biplanar by construction; the
13-vertex clique-cover encoding is validated by relaxing `ω ≤ 5` to `ω ≤ 6`,
where the Ore composition of two `K7`s must be recovered.

**Symmetry breaking is where soundness goes to die.** Lex-leader and
canonical-form constraints are the highest-risk part of any encoding here,
because an error in them silently removes solutions rather than throwing.
Where they are used, they are stated explicitly with their soundness argument
(see the header of `runs/run10_rt_sym.py`), and they are omitted entirely when
the variable count is small enough not to need them.

**Watch the direction of relaxations.** Dropping a derived constraint admits
more solutions, which is the safe direction for an UNSAT claim. Adding one is
not. The n=16 work is deliberately run over the full edge range `[36,39]`
rather than the value pinned by Kostochka–Yancey, so the closure depends on no
citation at all.

**Independent re-implementation, not just a second run.** Headline closures are
re-decided by `runs/recheck_cegar.py`, which builds its CNF from separately
written generators, and cross-checked under two solvers (Cadical and Glucose).

Two technical notes worth carrying forward. The max-closure formulation of
"max over `S` of `e(S) − 6|S|`" returns 0 for every graph, since the empty set
attains it; the correct exact tool for the hereditary bound is the (6,12)
pebble game. And `α = q` means the complement is `K_{q+1}`-free, so the
parameter passed to the Ramsey–Turán deciders is `q`, not `q+1`.

## Where the live edges are

- **n = 16**, six remaining profiles. The clearest finishable result.
- **The α=2 region at n = 19** is being *exhausted* rather than sampled
  (`f085`). Andrásfai pins the window to `m(G) ∈ [98,102]`; several thousand
  Euler-tight graphs are decided non-biplanar so far, with zero witnesses.
- **`RT` values for `q = 3, 4`** have no literature and must be computed
  in-house. The highest-leverage unknown is `RT(30, K₄, 6)`.
- **`rt37` and `rt38`** are the roomiest concrete candidates ever produced
  here (`f079`). Both survive every localized bound, and `rt38` sits *exactly*
  on the L2 boundary at 144/144.
- **The α=3 route** looks jointly impossible but is not proved so (`f063`).
  Each constraint alone is easy to satisfy; the conjunction never is.

## Verifying anything here

`tools/verify.py` is the shared verifier: planarity with Kuratowski
certificates, exact chromatic number by SAT, and exact biplanar splitting by
branch and bound. It ships with controls (`--controls`). `tools/rlog.py brief`
prints the session brief, and `rlog.py check --family X` answers whether a
family has already been ruled out.

The ledger is append-only. A claim is never deleted, only superseded by a
later finding naming it in `supersedes`, so the record keeps the argument
rather than just the answer.