# For future LLMs: state of the art You are probably here because someone asked you to work on the Earth–Moon problem, or handed you this repository. This file is written to get you to the research frontier in one read, so you do not spend your context rediscovering what is already settled. - Repository: `https://github.com/seanstock/tenchromacolonies` - Live site: `https://sean.wiki/colorthecolonies/` - Full record: [`data/ledger/LEDGER.md`](data/ledger/LEDGER.md) — every claim with its evidence, organised by category - Short version: [`HIGHLIGHTS.md`](HIGHLIGHTS.md) - Operating brief: [`PROMPT.md`](PROMPT.md) — read before proposing anything Run `./tools/rlog.py brief` first. It prints the hard bounds, the closed families with reasons, working techniques, and open questions. Then `rlog.py check --family X` before committing to any family; it will block one the ledger has closed, and you may proceed only by naming the new idea that breaks the stated reason. --- ## 1. The problem, precisely A graph `G = (V, E)` is **biplanar** (equivalently, has thickness ≤ 2) if `E = E₁ ∪ E₂` with both `(V, E₁)` and `(V, E₂)` planar on the same vertex set. The **Earth–Moon problem** asks for the maximum chromatic number over all biplanar graphs. The name comes from map colouring: each country has a colony on the Moon, and countries sharing a border on either world need different colours. **Known bounds: `9 ≤ χ ≤ 12`.** Both have been stuck for decades. - Upper bound 12: `m ≤ 6n − 12` forces minimum degree ≤ 11, so biplanar graphs are 11-degenerate and `χ ≤ 12`. - Lower bound 9: Sulanke's `K6 + C5` (11 vertices, 50 edges, χ = 9), from the 1970s, still the record. - Kirchweger, Scheucher and Szeider (SAT 2023) proved by computer search that every biplanar graph on `n ≤ 13` vertices is 9-colourable. **The open question this repo attacks: does a biplanar graph with χ ≥ 10 exist?** It was not found here. 742 candidates were logged, 717 verified, 699 died on planarity. ## 2. The two hard bounds — check these before proposing anything Any 10-chromatic biplanar witness `G` on `n` vertices with `m` edges must satisfy both: ``` Euler ceiling m <= 6n - 12 two planar layers cannot carry more Criticality floor m >= ceil(9n/2) a 10-critical graph has min degree >= 9 ``` The corridor between them is non-empty only for `n ≥ 8`. At `n = 30` it is `135 ≤ m ≤ 168`. **A very large fraction of proposals die to this arithmetic alone.** Compute it before doing anything else. ## 3. Families that are CLOSED — do not retry without a new structural idea | family | finding | why it dies | |---|---|---| | `K_a + C_b` joins (b odd) | `f002` | counting forces `K7+C3 = K10`, which contains `K9`; no biplanar graph contains `K9` | | Mycielskians (single-step, plain) | `f003` | `m' ≥ 13n_H > 6n' − 12` always | | cycle powers `C_n^k` | `f012` | closed for all `n, k` by ceiling or by arc-colouring giving χ ≤ 9 | | Kneser graphs (full) | `f013` | regular of degree ≥ 45 against average degree < 12 | | shift graphs | `f014` | χ = ⌈log₂ n⌉ ≥ 10 needs n ≥ 513, far past the ceiling | | quadrangulation doubling | `f016` | triangle-free layers give `m ≤ 4n−8` < floor | | odd-cycle blowups | `f026`, `f011` | all four survivors killed by the triangle-free band bound | | circulants, every region | `f039`, `f074`, `f075` | 150,457 connection sets enumerated, zero qualify | | α=2 join `t=2`, n=15..19 | `f078` | `Δ ≤ α` in triangle-free graphs gives `RT(n,K₃,s) ≤ ⌊ns/2⌋` | Sparse chi-critical subgraphs of Kneser graphs (e.g. Schrijver `SG(12,2)`: 54 vertices, χ = 10, ω = 6) are **not** covered by `f013` and remain open. ## 4. The main structural results **Localized biplanarity bounds (`f045`).** The workhorse. In any biplanar `G`, for every vertex subset `S` with `|S| ≥ 3`: ``` (L1) e(G[S]) <= 6|S| - 12 hereditary Euler (L2) triangle-free H spanning h vertices: e(H) <= 4h - 8 (L3) 2e(H) - t(H) <= 8h - 16 t = triangle count ``` L2 is the one that kills things: it closed the odd-cycle blowup family and eliminated 979 of 1000 candidates in a single sweep (`f047`). **The Ramsey–Turán unification (`f076`).** Every unresolved region of every attack route is the same extremal question. Write `Ḡ` for the complement. A witness with `α(G) ≤ q` needs `Ḡ` to be `K_{q+1}`-free; `K9`-freeness needs `α(Ḡ) ≤ s`; the Euler budget becomes `m(Ḡ) ≥ need`. So each region is an instance of ``` RT(n, K_{q+1}, s) = max edges of a K_{q+1}-free graph on n vertices with independence number at most s ``` A region closes with **no graph search at all** whenever `RT < need`. This also diagnoses every failure observed: the binding constraint was never edge count but independence, because Turán-extremal `K_{q+1}`-free graphs have `α = ⌈n/q⌉`, which is 8–11 at these sizes against the 6–8 required. **Careful with the parameter:** `α = q` means the complement is `K_{q+1}`-free. The deciders take `q`, not `q+1`. **Andrásfai's theorem gives exact values (`f081`).** For `q = 2` the quantity above 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 yields `RT(17,K₃,7) = 58` and `RT(19,K₃,8) = 73`, which pin the α=2 search window exactly. **No analogous literature exists for `q = 3, 4`;** those values must be computed in-house. **The minimum-degree shortcut is dead (`f071`).** Since every 10-critical graph has δ ≥ 9 and biplanarity is hereditary, "no biplanar graph has minimum degree 9" would have settled the problem at χ = 9. It is false: biplanar graphs with minimum degree 9, 10 and 11 all exist and were built in seconds (`runs/out/MINDEG*.json`). All of them have χ = 6. **No impossibility proof can route through degeneracy.** **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), Open Problem 3 asks for the thickness of inflated cycles; the band bound settles the lower-bound half. ## 5. The low-order programme — the most citable line Showing no 10-critical **core** exists on `n` vertices proves every biplanar graph on `n` vertices is 9-colourable. Published state is `n ≤ 13`. Closed here: | n | finding | method | |---:|---|---| | 13 | `f051` | exhaustive enumeration of subcubic complements; max 10 edges < 12 needed | | 14 | `f054` | matching-number case split + CEGAR; max 17 < 19 needed | | 15 | `f052` | Gallai join-decomposition, 11 cases, all over the ceiling | | 17 | `f055` | clique-kill chain forces triangle-free complement, dies at 45 < 46 | | 18 | `f060` | the three concrete candidates only, **not** the whole regime | **n = 16 is the live gap** (`f084`, `f086`, `f087`). The reduction: the complement `H` needs `Δ(H) ≤ 6`, savings `s(H) ≤ 6`, `α(H) ≤ 8`, `m(H) ≥ 36`. Because savings dominate the matching number, `s(H) ≤ 6` forces `ν(H) ≤ 6` and deficiency ≥ 4, so Berge–Tutte splits the problem into 14 component profiles. Complementation turns those components into a **join**, and χ of a join is exactly the sum of the parts', so the requirement becomes a budget on the parts' clique cover numbers. Bounding those arithmetically (Kostochka–Yancey, Brooks, ω of the complement) kills 8 of the 14 profiles by counting alone. Six survive, all of shape "one big component plus isolated vertices": `a=0/[13,1,1,1]`, `a=1/[11,1⁴]`, `a=1/[10,1⁵]`, `a=2/[9,1⁵]`, `a=2/[8,1⁶]`, `a=3/[7,1⁶]`. Closing all six extends the published result to `n ≤ 17`. The hardest, `a=0`, reduces to a single 13-vertex question: **is there a graph on 13 vertices with δ ≥ 6, at most 42 edges, no `K6`, and χ ≥ 7?** Note that 7-chromatic `K6`-free graphs do exist on as few as 11 vertices (the vertex Folkman number `F_v(2₆;6) = 11`, Nenov 2009, extremal graph `K₁ + C₅ + C₅`), so no vertex-count argument closes it. Kostochka–Yancey's non-Ore bound (Combinatorica 38 (2018) 887–934, Thm 6) pins the edge count to exactly 42. **This specific question is not answered in the literature.** ## 6. Techniques that work **The Euler-tight encoding (`f036`).** When `m = 6n − 12` exactly, both layers are forced to be triangulations. Add per-vertex layer-degree bounds, per-edge same-layer triangle support, monochromatic `K5`/`K3,3` bans and Euler counting windows: the seed CNF is then propositionally UNSAT at round zero, with no Kuratowski refinement at all. This is why thousands of Euler-tight candidates decide in seconds each. **CEGAR for biplanarity** (`runs/cegar.py`). One variable per edge, seeded with no-monochromatic-`K5`/`K3,3` clauses, Kuratowski subdivisions added lazily. Flags: `--tight`, `--case-size1`, `--symbreak`, `--cuts-in`. **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, while the full clause set is one short clause per partition into 6 blocks and `S(13,6) = 9,321,312` is entirely postable. Stream clauses straight into the solver so the memory cost lands in the solver rather than in Python. **Product bound (`f067`).** `χ(G₁ ∪ G₂) ≤ χ(G₁) · χ(G₂)`. ## 7. Verification standard — meet this or your result will not be accepted 1. **Positive control, same code path.** Every decider must re-find a graph known to exist. Without that, an UNSAT is worthless. The biplanarity encodings use `double_tri_19` (biplanar by construction); the 13-vertex clique-cover encoding relaxes `ω ≤ 5` to `ω ≤ 6` and must recover the Ore composition of two `K7`s. 2. **Two solvers.** Cross-check under Cadical and Glucose. 3. **Independent re-implementation.** `runs/recheck_cegar.py` rebuilds the CNF from separately written generators. 4. **Relax, do not tighten.** Dropping a derived constraint admits more solutions, which is safe for UNSAT. Adding one is not. 5. **Symmetry breaking is the highest-risk component.** State its soundness argument explicitly, or omit it when the variable count is small. If you find an actual witness, follow the CLAIMING A RESULT protocol in `PROMPT.md` before announcing anything. ## 8. Where to work | target | why it is worth doing | |---|---| | the six remaining n=16 profiles | the clearest finishable result; extends the published bound to n ≤ 17 | | α=2 at n=19, complete exhaustion | Andrásfai pins the window to `m(G) ∈ [98,102]`; thousands decided non-biplanar, zero witnesses (`f085`) | | `RT(n, K₄, s)` for q=3, 4 | no literature exists; highest-leverage unknown is `RT(30, K₄, 6)` | | `rt37`, `rt38` | roomiest concrete candidates ever produced here; both survive every localized bound, and `rt38` sits exactly on the L2 boundary at 144/144 (`f079`) | | the α=3 route at n=28..30 | each constraint alone is easy, the conjunction never satisfiable; conjecture stated in `f063` | | Schrijver `SG(12,2)` critical subgraphs | not covered by the Kneser closure | ## 9. Two traps The max-closure formulation of "max over `S` of `e(S) − 6|S|`" returns 0 for every graph, because the empty set attains it. The correct exact tool for the hereditary bound is the **(6,12) pebble game**. Turán-extremal graphs have large independence number. If your construction maximises edges, it is almost certainly failing the independence constraint, which is the binding one in every region here. --- ## Environment Pure-Python toolchain: a virtualenv with `networkx` and `python-sat`. On Windows use WSL if pysat wheels misbehave. Run scripts with `RLOG_RUN` set to your session tag so the ledger attributes work correctly. `tools/verify.py` is the shared verifier: planarity with Kuratowski certificates, exact χ by SAT, exact biplanar splitting by branch and bound, with controls under `--controls`. Memory discipline: cap roughly 10–30 heavy solvers at once.