# Level Resolution Experiments

Computational investigation of a structural proof strategy for the four
color theorem via *level resolutions* of maximal planar graphs.

See `paper.tex` for full definitions, conjectures, and findings.

## Files

### Core library
- `level_cycles.py` — levels, level subgraphs, level cycles, resolution
  enumeration (used by old-definition coverage).
- `triangulation_gen.py` — vertex-insertion + flip closure (good to n=10).
- `triangulation_gen_fast.py` — WL-hash pre-filter for n ≥ 11.
- `balanced_layout.py` — Tutte-init random-search planar layout.
- `four_color.py` — level 4-coloring via parity 2-coloring of L_k.

### Experiments
- `coverage_new_def.py` — **coverage under the cleaner definition**:
  G' is a level resolution of G via S iff its parity subgraphs are
  bipartite. Reachability reduces to "G' admits a bipartite 2-partition
  with cardinality matching some BFS-realizable parity split."
- `coverage.py`, `coverage_fast.py`, `coverage_chunked.py` — coverage
  under the OLD (stricter) definition involving specific edge flips on
  level cycles.
- `face_counting.py` — per-target preimage counts (N_iso, N_paths) under
  the old definition.
- `orbit_check.py` — orbit-counting with k-flip reverse-preimages (used
  for old-definition icosahedron analysis).

### Visualizations
- `plot_oct.py`, `n7_examples.py`, `four_color_viz.py`.

## Summary under the new definition

| n  | iso-classes | reachable | md4 reachable |
|----|-------------|-----------|---------------|
| 6  | 2           | 2         | 1/1           |
| 7  | 5           | 5         | 1/1           |
| 8  | 14          | 14        | 2/2           |
| 9  | 50          | 50        | 5/5           |
| 10 | 233         | 233       | 12/12         |
| 11 | 1249        | 1249      | 34/34         |
| 12 | icosahedron | reachable | yes           |

**Every iso-class is reachable** at every tested size. The previously
"uncovered" classes T1 (n=7) and T6 (n=8) under the old definition are
both reachable under the cleaner definition.

The new definition makes coverage equivalent to 4CT plus a BFS-realizable
partition cardinality constraint, raising the question of what additional
structure on the preimage G would make the framework non-circular.

## Dependencies

```
pip install networkx matplotlib numpy scipy
```