Files
math-research/papers/level_resolutions_of_maximal_planar_graphs/experiments
didericis 8fde9494d8 Add small-n ELG counting experiment (iso, rooted)
count_elgs.py enumerates triangulation iso-classes and counts Even Level
Graphs (G,v) per n: iso-classes (sources up to Aut) and flag-rooted
(4E/|Aut| * s, an exact integer since Aut acts freely on flags).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
2026-05-22 12:20:18 -04:00
..

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.pycoverage 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