# Task brief — a 10-chromatic biplanar graph

You are working on a hard combinatorial construction problem. Treat it as a
research engineering task, not a lookup task. You are running in this
directory; the research log tool is `./tools/rlog.py`, the verifier is
`tools/verify.py`, all data lives under `data/`, and session scripts go in
`runs/`. Python (with networkx and pysat installed) is `.venv/bin/python`.

## GOAL

Construct a graph G = (V, E₁ ∪ E₂) on a single vertex set, where (V,E₁) and
(V,E₂) are each planar, and χ(G) ≥ 10. Equivalently: a graph of thickness ≤ 2
with chromatic number ≥ 10. This is the lower-bound side of the Earth–Moon
problem. The known bounds are 9 ≤ χ ≤ 12, so a witness would be a new result;
a session that instead proves constraints and closes families is also a
success, provided the ledger records it.

## DATA STATE

Everything in `data/` is real research, logged by verified computation.
`data/sample/` is a synthetic demo dataset used to develop the visualizer —
its attempts are fake and its findings fictional. Never read it back into the
log.

## BACKGROUND FACTS

These are established results. Your verifier reproduces them as controls (see
VERIFIER); after that, use them freely.

1. **K8 is biplanar and χ(K8) = 8.** (28 edges; 6n−12 = 36.)
2. **K9 is not biplanar**, even though it passes the edge count (36 ≤ 42).
   Beineke–Harary: θ(K_n) = ⌊(n+7)/6⌋ for all n except 9 and 10, where θ = 3.
3. **The known 9-chromatic biplanar graph is K6 + C5** (join; Sulanke):
   n = 11, m = 15 + 5 + 30 = 50 ≤ 54 = 6n−12, χ = 6 + 3 = 9.

Two consequences of fact 2 shape the whole search:

- **The counting bound is necessary, never sufficient.** K9 clears 6n−12
  comfortably and is still not biplanar. A candidate that survives the
  arithmetic is "not yet excluded", nothing more.
- **The witness must be K9-free.** Thickness is monotone under subgraphs, so
  no biplanar graph contains K9. Any witness has ω ≤ 8 while needing χ ≥ 10 —
  you are looking for a graph with χ − ω ≥ 2, and you cannot force the tenth
  colour with a clique. This favours families where chromatic number outruns
  clique number — Mycielskian-type, Kneser-type, shift-graph constructions —
  over anything built by piling on a bigger clique.

## NECESSARY CONDITIONS — DERIVE THESE BEFORE GENERATING ANYTHING

Write down the admissible region first, and be precise about which object each
bound applies to.

**Euler ceiling.** A simple planar graph on n ≥ 3 vertices has at most 3n − 6
edges, so any biplanar graph has

    m ≤ 6n − 12

This applies to every candidate, without exception.

**Criticality floor.** Every 10-chromatic graph contains a 10-critical
subgraph, and a subgraph of a biplanar graph is biplanar — so search directly
for the critical witness. It has minimum degree ≥ 9, hence

    m ≥ ⌈9n/2⌉        (for the 10-critical core)

**The corridor.** Both bounds hold together only for n ≥ 8:

| n  | floor ⌈9n/2⌉ | ceiling 6n−12 | width |
|----|--------------|---------------|-------|
| 8  | 36           | 36            | 0     |
| 13 | 59           | 66            | 7     |
| 17 | 77           | 90            | 13    |
| 30 | 135          | 168           | 33    |
| 60 | 270          | 348           | 78    |

This ⌈9n/2⌉ … 6n−12 corridor is what `rlog.derive_verdict()` enforces (a
candidate outside it is logged `infeasible`) and what every plate draws.
Testing membership is free — do it before you build the graph, not after.

**Sharper bounds, on paper.** Two published results tighten the region beyond
what the logger enforces; use them in analysis and findings:

- Gallai: a k-critical graph other than K_k has n ≥ k + 2. The core here
  cannot be K10 (K10 ⊃ K9), so **n ≥ 12** — nothing below 12 vertices need
  ever be generated.
- Kostochka–Yancey: a 10-critical graph has **m ≥ (88n − 70)/18 ≈ 4.89n**,
  strictly above the ⌈9n/2⌉ floor.

**Layer pinning.** If a candidate has m edges, then since neither layer
exceeds 3n − 6, each layer carries at least m − (3n − 6) edges. Near the top
of the corridor both layers are forced to be near-maximal planar —
near-triangulations, dense in triangles. That sits awkwardly against the
K9-free requirement. Work out what it implies before you generate.

Push further than this list. A proved obstruction removes a region; a tested
candidate removes a point. Anything you can establish — a counting argument on
the layer split, a consequence of K9-freeness, a parity or girth obstruction —
is worth more than a hundred candidates. Log each as a `constraint` finding.

## WORKED EXAMPLE — THE STANDARD OF RIGOUR EXPECTED

The clique-join-odd-cycle family closes on paper. For G = K_a + C_b (b odd,
b ≥ 3), χ(G) = a + 3, so χ ≥ 10 requires a ≥ 7. With n = a + b and
m = C(a,2) + b + ab, requiring m ≤ 6n − 12 gives

    a(a−1)/2 + ab − 6a − 5b + 12 ≤ 0

    a = 7:  2b − 9 ≤ 0  ⟹  b = 3
    a = 8:  3b − 8 ≤ 0  ⟹  no odd b ≥ 3
    a > 8:  strictly worse

The only survivor is K7 + C3 = K10, and θ(K10) = 3. No clique-join-odd-cycle
can be a 10-chromatic biplanar graph. The whole family is closed by two lines
of counting plus one known theorem, before a single candidate is built or a
solver invoked.

The same computation at a = 6 gives b ≤ 9: survivors b ∈ {3,5,7,9}, one of
which is K9, and K6 + C9 is exactly tight at m = 78 = 6n − 12, forcing both
layers to be exact triangulations.

Log this closure as a `ruled_out` finding for the join family, with the
arithmetic in the claim (see the log rules for how a paper closure cites
evidence). Then do the same kind of analysis for every family you consider,
before generating. Several families die on paper; that is the cheapest
possible outcome and you should be actively hunting for it.

## THE VERIFIER IS PROVIDED — VALIDATE IT, THEN USE IT

`tools/verify.py` is shared infrastructure, like rlog. It gives you:

- `planar(edges)` — planarity with a Kuratowski certificate on failure. Keep
  the certificate in the attempt's `why`: "not planar" is not a finding;
  "layer 2 has a K5 subdivision on the apex set" is (`kuratowski_kind` names
  the minor).
- `chi_sat(n, edges)` / `chi_ge(n, edges, k)` — exact chromatic number via
  SAT with greedy-clique precolouring for symmetry breaking; χ ≥ 10 means
  UNSAT at k = 9, and a SAT result at k = 9 is a proof of failure with the
  reason attached — read it (see APPROACH). `dsatur` and `greedy_clique` give
  cheap bounds before the solver.
- `biplanar_split(n, edges)` — exact B&B: finds a two-planar-layer partition
  or proves none exists. It is exponential; use it on small controls and
  structured cores, not inside generation loops.

**Extend it, don't rewrite it.** Sessions must stay comparable, so improve the
shared module in place (and note it in a `technique` finding). The single
exception: the CLAIMING A RESULT protocol requires re-verification through an
independent implementation — never reuse verify.py for that step.

**Controls, at the start of every session**:
`.venv/bin/python tools/verify.py --controls` checks K5 → 5, C11 → 3, K8 → 8
with an explicit planar 2-split, K6 + C5 → 9 and biplanar. The χ checks are
milliseconds; the K6 + C5 split search is the slow one (~1–2 min). Run-01
logged all of these as `control=True` attempts (a00001–a00007) with a
`milestone` finding — re-log only if verify.py changed. The K9 → not biplanar
refutation is deliberately excluded (`--k9` to include): it is an exhaustive
hours-long computation, tracked in the queue.

**Construct layers, don't split unions.** Deciding whether a given graph has
thickness ≤ 2 is NP-hard. Build the two layers and take their union. Families
that work the other way round ("random dense seed, then repair the split") are
legitimate but expensive; log the repair-loop cost so the ledger shows what
they actually cost.

## THE RESEARCH LOG IS PART OF THE TASK

A search that does not remember itself pays for every dead end twice. The tool
is `./tools/rlog.py` (run it from this directory; it resolves `data/` itself).
Set a run id once per session: `export RLOG_RUN=run-01` (increment per
session).

1. `./tools/rlog.py brief` — first command, before you propose anything. It
   prints the hard bounds, every family already ruled out and why, the
   techniques that worked, the open questions, the family scoreboard, the
   nearest misses and the next-action queue. If it contradicts an idea you
   were about to try, that contradiction is the most valuable thing in your
   context.

2. `./tools/rlog.py check --family <id>` before committing to a family. It
   reports what has been tried and whether a `ruled_out` finding blocks it.
   You may proceed against a block only by stating, in the candidate's `why`,
   what new structural idea breaks the stated reason. "Same family, different
   parameters" is not a new idea.

3. **Log every candidate you actually test — including failures.** Do this
   from inside your search loop by importing the module; do not shell out per
   candidate or write JSON by hand:

    ```python
    import sys; sys.path.insert(0, "tools")
    import rlog
    rlog.log(rlog.record(
        family="mycielski-hybrid",
        construction="M(C5) blown up, apex carried by layer 2",
        layers=[e1, e2],          # edge lists, one per intended planar layer
        planar=[True, False],     # results of your own planarity check
        chi=9,                    # if proved; None otherwise
        solver_ms=1840,
        why="layer 2 has a K5 subdivision on {0,3,7,11,14}; the apex edges all "
            "landed in the same layer"))
    ```

    That is the entire per-candidate burden (~0.4 ms). n, m, per-layer sizes,
    degrees, min_degree, the id, the generation and the verdict are derived
    from what you passed; you never hand-classify a verdict.

4. `./tools/rlog.py finding --kind … --claim … --evidence a00123,a00456`
   whenever you conclude something durable. Kinds: `constraint`, `ruled_out`,
   `technique`, `open_question`, `milestone`. A `ruled_out` finding is refused
   by the tool unless it cites attempt ids. For a family closed on paper, log
   its boundary candidates as attempts first (the counting survivors — e.g.
   for the join family, K7 + C3 = K10) and cite those, with
   `--confidence proved` and the full argument in the claim.

5. `./tools/rlog.py render` at the end, to rebuild LEDGER.md and index.json.

Findings are append-only. A claim you later disbelieve is retired by a new
finding naming it in `supersedes`. The ledger keeps the argument, not just the
current answer.

## APPROACH

1. **Verifier and controls.** Nothing else happens first.
2. **Necessary conditions.** Derive the corridor, the layer pinning and the
   K9-free consequence. For each family under consideration, do the counting
   analysis before generating.
3. **Brainstorm ≥ 5 structurally distinct families**, weighted toward
   constructions where χ outruns ω: Mycielskians and iterated Mycielskians,
   Kneser and Schrijver graphs, shift graphs, triangle-free high-χ
   constructions augmented toward the corridor, quadrangulation doubling,
   circulant splits, triangulation + apex, random + repair. Check
   `./tools/rlog.py brief` first — some may already be closed.
4. **Generate, test, log.** Cheapest checks first: corridor membership, then
   min degree, then planarity per layer, then clique/DSATUR bounds, then SAT.
   Every failure gets a `why` naming the mechanism.
5. **Read the witness.** When SAT returns a 9-colouring, inspect it before
   moving on: which class is fattest, which high-degree vertices share a class
   with no common neighbour. Those non-adjacent pairs name the exact edges to
   add next. Pass `coloring=` and `clique=` to `record()` so the candidate
   keeps its full graph. Blind regeneration throws away information the solver
   has already paid for.
6. **Refine from evidence.** Perturb near misses rather than reseeding. Do not
   repeat a family that failed structurally without a new idea, and state the
   new idea in the record.

## OUTPUT CONTRACT

Append-only text. No database — the log is written once, read whole, never
joined across; a thousand candidates is under a megabyte.

    data/attempts.jsonl          one JSON object per line, one per candidate tested
    data/detail/<id>.json        full graph for rows flagged detail:true
    data/ledger/findings.jsonl   durable claims + the attempt ids that earned them
    data/ledger/queue.json       next actions, carried between sessions
    data/ledger/LEDGER.md        generated by `rlog.py render` — never hand-edited
    data/index.json              manifest: counts, families, featured ids

An attempt record as `rlog.record()` writes it to disk (you supply the seven
fields shown in the Python example above; everything else, including the
per-layer dicts, is derived):

    {
      "id": "a00413", "ts": 1755100000, "run": "run-03",
      "family": "mycielski-hybrid",
      "construction": "M(C5) blown up, apex carried by layer 2",
      "params": {"core": "C5", "blowup": 3},
      "parent": "a00398", "generation": 2,
      "mutation": "moved the apex star into layer 2",
      "n": 22, "m": 108,
      "min_degree": 9, "max_degree": 15,
      "layers": [{"idx": 1, "m": 58, "planar": true},
                 {"idx": 2, "m": 50, "planar": false}],
      "verdict": "fail_planarity",
      "chi_lb": 8, "chi_ub": null, "chi": null,
      "solver_ms": 1840, "cost_ms": 2310,
      "why": "layer 2 has a K5 subdivision on {0,3,7,11,14}; the apex edges all landed in the same layer",
      "control": false, "detail": false
    }

`verdict` is derived by `rlog.derive_verdict()` — outside the ⌈9n/2⌉ … 6n−12
corridor is `infeasible` before anything else is considered, a non-planar
layer is `fail_planarity`, and so on:

| verdict         | meaning                                              |
|-----------------|------------------------------------------------------|
| verified_target | χ ≥ 10 with both layers planar — the result          |
| baseline_ok     | a control reproduced its expected χ                  |
| fail_chromatic  | layers planar, but a ≤9-colouring was found          |
| fail_planarity  | a layer is not planar                                |
| infeasible      | rejected by a necessary condition before solving     |
| timeout         | the SAT budget was exhausted                         |

Pass `layouts`, `coloring` or `clique` to `record()` and it flips to
`detail: true` automatically, writing the full graph to a sidecar. Do that for
anything worth looking at: controls, nearest misses, instructive witnesses.

You never touch the visualizer. The plates read attempts.jsonl,
findings.jsonl and index.json and redraw themselves — no rendering step in
your loop, no image to produce, no HTML to write.

## CLAIMING A RESULT

If you log `verified_target`, stop and re-verify from a clean process before
saying anything:

1. Independent planarity check on each layer, from the edge lists as written
   to disk — not from the in-memory objects that produced them.
2. Independent SAT run proving k = 9 UNSAT, ideally with a different encoding
   or a different solver.
3. Confirm the union really is the union: no edge in both layers, none
   missing, vertex sets identical.
4. Dump both edge lists so a third party can check them without your code.

A false positive costs more than a hundred honest failures. The same applies
to a claimed impossibility proof: state the argument in full in the finding,
and say which step is weakest.

## RULES

- Every response includes runnable code and at least one new candidate
  actually tested and logged, or a proved constraint that closes a region.
- Prefer closing a family on paper to testing it. Report proofs as findings
  with `confidence: proved`.
- Do not report a family as promising without an attempt id.
- "Clears the edge count" is not "passing" — it is "not yet excluded".
- Cite a specific result only when you are using it, and say whether you
  verified it computationally or are using it as stated in this brief.
- No meta-commentary on the difficulty of the problem, and no literature
  summaries.