didericis/math-research
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update level_resolutions paper: extend to n=12, add exploratory experiments

Browse Source 
- Update abstract and coverage table: computational evidence now includes n=12
  (previously n=6..11). All iso-classes remain reachable.
- Correct conjecture statement: minimum degree ≥5 (not ≥4).
- Add graphicx package (for potential figure support).
- Add exploratory experiment files for exception characterization, preimage
  search, and visualization (directed toward understanding the full orbit
  of the T*_9 case and related structural questions).

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
This commit is contained in:
didericis
2026-05-22 00:45:45 -04:00
parent bb144f069e
commit 79bfd8e588
16 changed files with 1642 additions and 175 deletions
Download Patch File Download Diff File Expand all files Collapse all files
papers/level_resolutions_of_maximal_planar_graphs/experiments/characterize_exception_family.py
+125
View File
@@ -0,0 +1,125 @@
"""Characterize the exception family for Lemma 5.8.
For each exception (md4 iso-class without a good contraction) at n=9..12,
extract:
1. The deg-4 vertices and whether they form 2 disjoint triangles
2. The high-degree "core" and its edge structure
3. The bipartite-like structure between deg-4 set and core
4. Whether the exception is constructed by some uniform recipe
"""
import sys, os
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import networkx as nx
from collections import Counter, defaultdict
from triangulation_gen import enumerate_all_triangulations
from triangulation_gen_fast import enumerate_all_triangulations_fast
def is_md4(T):
return min(T.degree(v) for v in T.nodes()) >= 4
def good_contractions_for_vertex(T, v):
if T.degree(v) != 4:
return []
ip, emb = nx.check_planarity(T)
if not ip:
return []
cyc = list(emb.neighbors_cw_order(v))
if len(cyc) != 4:
return []
a, b, c, d = cyc
good = []
for (u, w, opp1, opp2) in [(a, c, b, d), (b, d, a, c)]:
if T.has_edge(u, w):
continue
if T.degree(opp1) - 1 < 4 or T.degree(opp2) - 1 < 4:
continue
good.append((u, w))
return good
def has_good_contraction(T):
for v in T.nodes():
if good_contractions_for_vertex(T, v):
return True
return False
def find_exceptions(n):
if n >= 11:
isos = enumerate_all_triangulations_fast(n)
else:
isos = enumerate_all_triangulations(n)
md4_indices = [i for i, T in enumerate(isos) if is_md4(T)]
exceptions = []
for i in md4_indices:
T = isos[i]
# Skip md5+ (no deg-4 vertex, so contraction trivially N/A)
if not any(T.degree(v) == 4 for v in T.nodes()):
continue
if not has_good_contraction(T):
exceptions.append((i, T))
return exceptions
def analyze_exception(T, label=""):
"""Print structural analysis of an exception triangulation."""
deg4 = [v for v in T.nodes() if T.degree(v) == 4]
high = [v for v in T.nodes() if T.degree(v) >= 5]
print(f" {label}: |deg-4|={len(deg4)}, |high|={len(high)}")
# Subgraph on deg-4 vertices
Td4 = T.subgraph(deg4)
deg4_edges = sorted(Td4.edges())
print(f" deg-4 subgraph edges: {deg4_edges}")
# Find triangles in deg-4 subgraph
triangles = []
deg4_set = set(deg4)
for v in deg4:
for u in deg4:
if u >= v:
continue
for w in deg4:
if w >= u:
continue
if T.has_edge(v, u) and T.has_edge(u, w) and T.has_edge(v, w):
triangles.append(tuple(sorted([v, u, w])))
triangles = sorted(set(triangles))
print(f" triangles within deg-4 set: {triangles}")
# Each deg-4 vertex's high-degree neighbors
print(f" deg-4 vertices -> their high-degree neighbors:")
for v in deg4:
hi_nbrs = sorted(u for u in T.neighbors(v) if T.degree(u) >= 5)
print(f" {v}: {hi_nbrs}")
# Subgraph on high-degree vertices
Thigh = T.subgraph(high)
high_edges = sorted(Thigh.edges())
high_degs = {v: Thigh.degree(v) for v in high}
print(f" high-degree subgraph edges: {high_edges}")
print(f" high-degree subgraph degrees: {high_degs}")
# Bipartite-like check: each deg-4 vertex has exactly 2 high neighbors?
deg4_high_counts = Counter()
for v in deg4:
hi_nbrs = [u for u in T.neighbors(v) if T.degree(u) >= 5]
deg4_high_counts[len(hi_nbrs)] += 1
print(f" # deg-4 vertices grouped by # high neighbors: "
f"{dict(deg4_high_counts)}")
# Each high vertex's deg-4 neighbors
print(f" high vertices -> # deg-4 neighbors:")
for h in high:
d4_nbrs = [u for u in T.neighbors(h) if T.degree(u) == 4]
print(f" {h} (deg {T.degree(h)}): {len(d4_nbrs)} deg-4 nbrs")
def main():
for n in [9, 10, 11, 12]:
print(f"\n=== n={n} ===")
exceptions = find_exceptions(n)
print(f" {len(exceptions)} exception(s) (excluding md5+)")
for idx, T in exceptions:
print(f"\n iso[{idx}]:")
analyze_exception(T)
if __name__ == "__main__":
main()
papers/level_resolutions_of_maximal_planar_graphs/experiments/coverage_new_def.py
+4 -1
View File
@@ -100,5 +100,8 @@ def analyze(n, use_fast=False, verbose=True):
if __name__ == "__main__":
for n in [6, 7, 8, 9, 10, 11]:
import sys
ns = [int(x) for x in sys.argv[1:]] if len(sys.argv) > 1 \
else [6, 7, 8, 9, 10, 11]
for n in ns:
analyze(n, use_fast=(n >= 11))
papers/level_resolutions_of_maximal_planar_graphs/experiments/find_icosa_preimage_broad.py
+147
View File
@@ -0,0 +1,147 @@
"""Broader search for an icosahedron preimage at n=12.
Key changes from find_icosa_preimage_fast:
- Increase branching limits (p1_branch=8, p2_branch=8, cap=65536)
- Filter outputs by 5-regularity (faster than full iso check)
Note: any 5-regular planar triangulation on 12 vertices IS iso to the
icosahedron (unique 5-regular triangulation at this size)
- Report progress every 100 iso-classes
"""
import sys, os, time
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import networkx as nx
from collections import defaultdict
from itertools import product as iproduct
from triangulation_gen_fast import enumerate_all_triangulations_fast
from level_cycles import compute_levels, level_sources
from depth_monovariant_check import (
faces_of_subgraph, canonical_face, edges_of_face,
apex_levels_for_edge, identify_outer_face,
)
from full_resolution_check import phase1_resolve_isolated
from simple_level_resolution_coverage import (
break_source_triangle, all_source_triangle_breaks,
phase2_outer_incident_choices, apply_phase2_choices,
phase1_branch, is_triangulation,
)
def is_5_regular(G):
return all(d == 5 for v, d in G.degree())
def simple_level_resolutions_broad(G, source_set, p1_branch=8, p2_branch=8,
cap=2048):
"""Same as simple_level_resolutions but with wider branching."""
levels = compute_levels(G, source_set)
by_level = defaultdict(list)
for v, lv in levels.items():
by_level[lv].append(v)
seen_outputs = set()
for Gc in all_source_triangle_breaks(G, source_set):
for G_p1 in phase1_branch(Gc, levels, by_level,
branch_limit=p1_branch):
per_level_choices = []
for k in sorted(by_level):
if k == 0:
continue
if len(by_level[k]) < 3:
continue
nodes_k = by_level[k]
ip, emb = nx.check_planarity(G_p1)
if not ip:
continue
pcs = phase2_outer_incident_choices(G_p1, emb, levels,
nodes_k, k,
include_even=True)
pcs = [c[:p2_branch] for c in pcs]
per_level_choices.extend(pcs)
if not per_level_choices:
sig = tuple(sorted(G_p1.edges()))
if sig not in seen_outputs:
seen_outputs.add(sig)
yield G_p1
continue
total = 1
for c in per_level_choices:
total *= len(c)
if total > cap:
choices = [c[0] for c in per_level_choices]
Gp = apply_phase2_choices(G_p1, choices)
sig = tuple(sorted(Gp.edges()))
if sig not in seen_outputs:
seen_outputs.add(sig)
yield Gp
continue
for combo in iproduct(*per_level_choices):
Gp = apply_phase2_choices(G_p1, combo)
sig = tuple(sorted(Gp.edges()))
if sig not in seen_outputs:
seen_outputs.add(sig)
yield Gp
def main():
print("Loading n=12 iso-classes...")
t0 = time.time()
isos = enumerate_all_triangulations_fast(12)
print(f" {len(isos)} iso-classes loaded ({time.time()-t0:.1f}s)")
md5_idx = [i for i, T in enumerate(isos)
if all(d == 5 for _, d in T.degree())]
print(f" md5 iso-classes: {md5_idx}")
icosa = isos[md5_idx[0]]
found = []
start = time.time()
for src_idx, G in enumerate(isos):
if src_idx % 50 == 0:
elapsed = time.time() - start
print(f" [{src_idx}/{len(isos)}] ({elapsed:.1f}s) "
f"found={len(found)}", flush=True)
ip, emb = nx.check_planarity(G)
if not ip:
continue
for kind, lab, source_set in level_sources(G, emb):
count = 0
for Gp in simple_level_resolutions_broad(G, source_set):
count += 1
if count > 100:
break
if not is_triangulation(Gp, 12):
continue
if not is_5_regular(Gp):
continue
# Now Gp is iso to icosa (uniqueness of 5-regular at n=12)
levels = compute_levels(G, source_set)
even = [v for v in Gp.nodes()
if levels.get(v, 0) % 2 == 0]
odd = [v for v in Gp.nodes()
if levels.get(v, 0) % 2 == 1]
if not (nx.is_bipartite(Gp.subgraph(even)) and
nx.is_bipartite(Gp.subgraph(odd))):
continue
G_edges = set(frozenset(e) for e in G.edges())
Gp_edges = set(frozenset(e) for e in Gp.edges())
if G_edges == Gp_edges:
continue
found.append({
'src_idx': src_idx,
'source': (kind, lab),
'source_set': sorted(source_set),
})
print(f" FOUND PREIMAGE: src_iso={src_idx}, "
f"source=({kind}, {lab})")
if len(found) >= 3:
break
if len(found) >= 3:
break
if len(found) >= 3:
break
print(f"\nTotal preimages found: {len(found)} (elapsed {time.time()-start:.1f}s)")
for ex in found:
print(f" {ex}")
if __name__ == "__main__":
main()
papers/level_resolutions_of_maximal_planar_graphs/experiments/find_icosa_preimage_fast.py
+89
View File
@@ -0,0 +1,89 @@
"""Find any (G, S) at n=12 whose algorithm output is iso to the icosahedron,
record the symmetric difference, and test the cross-level conjecture."""
import sys, os
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import networkx as nx
from triangulation_gen_fast import enumerate_all_triangulations_fast
from level_cycles import compute_levels, level_sources
from simple_level_resolution_coverage import (
simple_level_resolutions, is_triangulation,
)
def is_md5(T):
return min(T.degree(v) for v in T.nodes()) >= 5
def main():
isos = enumerate_all_triangulations_fast(12)
md5_idx = [i for i, T in enumerate(isos) if is_md5(T)]
print(f"md5 iso-classes at n=12: {md5_idx}")
if len(md5_idx) != 1:
print(f"unexpected: not exactly 1 md5 class")
icosa = isos[md5_idx[0]]
print(f"icosahedron edges: {sorted(icosa.edges())[:8]}...")
# For each (G, S), check if algorithm output is iso to icosa.
found = []
for src_idx, G in enumerate(isos):
ip, emb = nx.check_planarity(G)
if not ip:
continue
for kind, lab, source_set in level_sources(G, emb):
count = 0
for Gp in simple_level_resolutions(G, source_set):
count += 1
if count > 30:
break
if not is_triangulation(Gp, 12):
continue
if not nx.is_isomorphic(Gp, icosa):
continue
# Require bipartite parity subgraphs (real simple level res)
levels = compute_levels(G, source_set)
even = [v for v in Gp.nodes() if levels.get(v, 0) % 2 == 0]
odd = [v for v in Gp.nodes() if levels.get(v, 0) % 2 == 1]
if not (nx.is_bipartite(Gp.subgraph(even)) and
nx.is_bipartite(Gp.subgraph(odd))):
continue
# Skip degenerate cases where algorithm did nothing
G_edges = set(frozenset(e) for e in G.edges())
Gp_edges = set(frozenset(e) for e in Gp.edges())
if G_edges == Gp_edges:
continue
added = Gp_edges - G_edges
removed = G_edges - Gp_edges
def lvl_diff(e):
u, v = tuple(e)
return abs(levels.get(u, -1) - levels.get(v, -1))
added_diffs = [lvl_diff(e) for e in added]
removed_diffs = [lvl_diff(e) for e in removed]
found.append({
'src_idx': src_idx,
'source': (kind, lab),
'source_set': sorted(source_set),
'added_count': len(added),
'removed_count': len(removed),
'added_diffs': sorted(added_diffs),
'removed_diffs': sorted(removed_diffs),
'added_all_cross': all(d >= 1 for d in added_diffs),
'removed_all_same': all(d == 0 for d in removed_diffs),
})
if len(found) >= 5:
break
if len(found) >= 5:
break
if len(found) >= 5:
break
print(f"\nfound {len(found)} preimages of icosahedron")
for ex in found:
print(f"\n src_iso={ex['src_idx']}, source={ex['source']}")
print(f" source set: {ex['source_set']}")
print(f" added={ex['added_count']} (level diffs {ex['added_diffs']}), "
f"removed={ex['removed_count']} (level diffs {ex['removed_diffs']})")
print(f" added all cross-level: {ex['added_all_cross']}; "
f"removed all same-level: {ex['removed_all_same']}")
if __name__ == "__main__":
main()
papers/level_resolutions_of_maximal_planar_graphs/experiments/find_md5_preimages.py
+108
View File
@@ -0,0 +1,108 @@
"""Find a working preimage for each md5 iso-class.
For each md5 target T at n, search (G, S) and branching choices to find
any G that the algorithm transforms to T (label-exact). Report:
- the preimage G
- the source S
- the edit distance from G to T (number of edges differing)
- what the differing edges look like
"""
import sys, os
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import networkx as nx
from itertools import permutations
from triangulation_gen_fast import enumerate_all_triangulations_fast
from triangulation_gen import enumerate_all_triangulations
from level_cycles import compute_levels, level_sources
from simple_level_resolution_coverage import (
simple_level_resolutions, is_triangulation, iso_index,
)
def is_md5(T):
return min(T.degree(v) for v in T.nodes()) >= 5
def find_one_preimage(target, isos, n):
"""Find any (G, S) producing target (label-exact). Try all relabelings."""
target_edges = set(frozenset(e) for e in target.edges())
target_nodes = list(target.nodes())
for G in isos:
if n > 7:
# Don't try all permutations for big n; just try a few.
from random import shuffle, seed
seed(42)
perms = []
for _ in range(50):
p = list(target_nodes)
shuffle(p)
perms.append(tuple(p))
else:
perms = list(permutations(target_nodes, n))
for perm in perms:
relabel = {orig: perm[i]
for i, orig in enumerate(sorted(G.nodes()))}
H = nx.relabel_nodes(G, relabel, copy=True)
ip, emb = nx.check_planarity(H)
if not ip:
continue
for kind, lab, source_set in level_sources(H, emb):
count = 0
for Hp in simple_level_resolutions(H, source_set):
count += 1
if count > 50:
break
if not is_triangulation(Hp, n):
continue
Hp_edges = set(frozenset(e) for e in Hp.edges())
if Hp_edges == target_edges:
return (H, source_set, Hp, kind, lab)
return None
def edit_distance(G1, G2):
"""Symmetric difference of edge sets."""
e1 = set(frozenset(e) for e in G1.edges())
e2 = set(frozenset(e) for e in G2.edges())
return e1 ^ e2
def main(ns):
for n in ns:
print(f"\n=== n={n} ===")
if n >= 11:
isos = enumerate_all_triangulations_fast(n)
else:
isos = enumerate_all_triangulations(n)
md5 = [(i, T) for i, T in enumerate(isos) if is_md5(T)]
print(f" {len(md5)} md5 iso-class(es)")
for idx, T in md5:
ds = sorted([T.degree(v) for v in T.nodes()], reverse=True)
print(f"\n iso[{idx}] ds={ds}")
print(f" T edges: {sorted(T.edges())[:8]}...")
result = find_one_preimage(T, isos, n)
if result is None:
print(f" NO preimage found in search")
continue
H, source_set, Hp, kind, lab = result
diff = edit_distance(H, T)
print(f" preimage source kind={kind}, label={lab}")
print(f" source set: {sorted(source_set)}")
print(f" edit distance H -> T: {len(diff) // 2} edge flip(s)")
print(f" edges only in H: "
f"{sorted(e for e in diff if e in [frozenset(x) for x in H.edges()])[:10]}")
print(f" edges only in T: "
f"{sorted(e for e in diff if e in [frozenset(x) for x in T.edges()])[:10]}")
# Inspect: are the differing edges on the source-face boundary?
a, b, c = tuple(source_set) if len(source_set) == 3 else \
(None, None, None)
if a is not None:
src_face_edges = {frozenset([a, b]), frozenset([b, c]),
frozenset([a, c])}
src_face_in_diff = src_face_edges & diff
print(f" src-face edges in diff: {sorted(src_face_in_diff)}")
if __name__ == "__main__":
ns = [int(x) for x in sys.argv[1:]] if len(sys.argv) > 1 else [12]
main(ns)
papers/level_resolutions_of_maximal_planar_graphs/experiments/good_contraction_lemma_check.py
+94
View File
@@ -0,0 +1,94 @@
"""Empirical check of Lemma 5.8 (good contraction).
For every md4 plane triangulation iso-class at n in {7, 8, 9, 10, 11},
verify that there exists a degree-4 vertex v with cyclic neighbors
(a, b, c, d) and a diagonal (a, c) such that:
(1) (a, c) is not an edge of T,
(2) deg(b) >= 5 and deg(d) >= 5.
Equivalently, the contracted triangulation T_{v, (a,c)} has min deg >= 4.
Reports:
- Total md4 iso-classes at each n
- How many have at least one good contraction
- Iso-classes without a good contraction (if any)
- For each iso-class, how many degree-4 vertices admit a good contraction
"""
import sys, os
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import networkx as nx
from triangulation_gen import enumerate_all_triangulations
from triangulation_gen_fast import enumerate_all_triangulations_fast
def is_md4(T):
return min(T.degree(v) for v in T.nodes()) >= 4
def cyclic_neighbors(G, v):
ip, emb = nx.check_planarity(G)
if not ip:
return None
return list(emb.neighbors_cw_order(v))
def good_contractions_for_vertex(T, v):
"""Return list of valid diagonals (u, w) such that contracting v
along (u, w) preserves md4."""
if T.degree(v) != 4:
return []
cyc = cyclic_neighbors(T, v)
if cyc is None or len(cyc) != 4:
return []
a, b, c, d = cyc
good = []
for (u, w, opp1, opp2) in [(a, c, b, d), (b, d, a, c)]:
if T.has_edge(u, w):
continue
# After contraction, opp1 and opp2 lose 1 degree each.
if T.degree(opp1) - 1 < 4:
continue
if T.degree(opp2) - 1 < 4:
continue
good.append((u, w))
return good
def check_n(n):
if n >= 11:
isos = enumerate_all_triangulations_fast(n)
else:
isos = enumerate_all_triangulations(n)
md4 = [(i, T) for i, T in enumerate(isos) if is_md4(T)]
total = len(md4)
with_good = 0
no_good = []
counts_per_class = []
for idx, T in md4:
deg4_verts = [v for v in T.nodes() if T.degree(v) == 4]
good_count_for_class = 0
for v in deg4_verts:
good = good_contractions_for_vertex(T, v)
if good:
good_count_for_class += 1
if good_count_for_class > 0:
with_good += 1
else:
no_good.append(idx)
counts_per_class.append(good_count_for_class)
print(f"n={n}: {total} md4 iso-classes")
print(f" with at least one good contraction: {with_good} / {total}")
if no_good:
print(f" iso-classes WITHOUT a good contraction: {no_good}")
if counts_per_class:
print(f" good-deg-4-vertices per class: "
f"min={min(counts_per_class)}, "
f"max={max(counts_per_class)}, "
f"median={sorted(counts_per_class)[len(counts_per_class)//2]}")
if __name__ == "__main__":
ns = [int(x) for x in sys.argv[1:]] if len(sys.argv) > 1 \
else [7, 8, 9, 10, 11]
for n in ns:
check_n(n)
papers/level_resolutions_of_maximal_planar_graphs/experiments/inspect_cross_level_failure.py
+119
View File
@@ -0,0 +1,119 @@
"""Take one failure case from the cross-level conjecture test and search
the full subset space of cross-level edges to find an iso(G)-recovering
subset, OR confirm no such subset exists."""
import sys, os
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import networkx as nx
from itertools import combinations
from triangulation_gen import enumerate_all_triangulations
from level_cycles import compute_levels, level_sources
from simple_level_resolution_coverage import (
simple_level_resolutions, is_triangulation,
)
from test_cross_level_iso_inverse import flip_edge, apply_flips
def find_first_failure(n):
"""Return the first (G, S, T) triple at n where no subset of size ≤ 6 of
inherited cross-level edges recovers iso(G)."""
isos = enumerate_all_triangulations(n)
for src_idx, G in enumerate(isos):
ip, emb = nx.check_planarity(G)
if not ip:
continue
for kind, lab, source_set in level_sources(G, emb):
count = 0
for Gp in simple_level_resolutions(G, source_set):
count += 1
if count > 4:
break
if not is_triangulation(Gp, n):
continue
G_edges = set(frozenset(e) for e in G.edges())
Gp_edges = set(frozenset(e) for e in Gp.edges())
if G_edges == Gp_edges:
continue
# Find cross-level inherited edges
levels = compute_levels(G, source_set)
algorithm_added = Gp_edges - G_edges
cross_in_T = {e for e in Gp_edges
if levels.get(tuple(e)[0], -1)
!= levels.get(tuple(e)[1], -1)}
cross_inherited = cross_in_T - algorithm_added
# Try all subsets up to size 6
found = False
for k in range(1, min(6, len(cross_inherited)) + 1):
if found:
break
for subset in combinations(cross_inherited, k):
T_flipped, _ = apply_flips(
Gp, [tuple(e) for e in subset])
if nx.is_isomorphic(T_flipped, G):
found = True
break
if not found:
return src_idx, kind, lab, source_set, G, Gp, levels, \
algorithm_added, cross_in_T, cross_inherited
return None
def exhaustive_search(G, Gp, cross_inherited, max_k=None):
"""Search all subsets of cross_inherited for one whose flip yields iso(G).
Returns the subset if found, else None."""
edges = list(cross_inherited)
if max_k is None:
max_k = len(edges)
for k in range(1, max_k + 1):
for subset in combinations(edges, k):
T_flipped, _ = apply_flips(Gp, [tuple(e) for e in subset])
if nx.is_isomorphic(T_flipped, G):
return subset
return None
def main():
print("Finding first failure at n=7...")
result = find_first_failure(7)
if result is None:
print("No failures found at n=7 (within max_k=6)")
return
src_idx, kind, lab, source_set, G, Gp, levels, algorithm_added, \
cross_in_T, cross_inherited = result
print(f"\n src={src_idx} source=({kind}, {lab})")
print(f" source set: {sorted(source_set)}")
print(f" G edges: {sorted(G.edges())}")
print(f" Gp (= T) edges: {sorted(Gp.edges())}")
print(f" G \\ T (removed): {sorted([tuple(e) for e in (set(frozenset(x) for x in G.edges()) - set(frozenset(y) for y in Gp.edges()))])}")
print(f" T \\ G (added by alg): {sorted([tuple(e) for e in algorithm_added])}")
print(f" G-levels: {dict(sorted(levels.items()))}")
print(f" cross-level edges in T: {sorted([tuple(e) for e in cross_in_T])}")
print(f" cross-level inherited (not added by algorithm): "
f"{sorted([tuple(e) for e in cross_inherited])}")
print(f" num inherited cross-level: {len(cross_inherited)}")
# Exhaustive search
print(f"\n Exhaustively searching all subsets of cross_inherited "
f"({2**len(cross_inherited)} subsets total)...")
subset = exhaustive_search(G, Gp, cross_inherited)
if subset is None:
print(f" NO subset of cross-level inherited edges recovers iso(G)")
else:
print(f" Found subset of size {len(subset)}: "
f"{sorted([tuple(e) for e in subset])}")
# Verify
T_flipped, _ = apply_flips(Gp, [tuple(e) for e in subset])
print(f" flipped graph edges: {sorted(T_flipped.edges())}")
print(f" iso to G: {nx.is_isomorphic(T_flipped, G)}")
# Also try the FULL set of cross-level edges (including algorithm-added)
print(f"\n Also trying full cross-level set (including algorithm-added)...")
subset2 = exhaustive_search(G, Gp, cross_in_T)
if subset2 is None:
print(f" Even using all cross-level edges, no recovery found")
else:
print(f" Found subset of size {len(subset2)} from full cross set: "
f"{sorted([tuple(e) for e in subset2])}")
if __name__ == "__main__":
main()
papers/level_resolutions_of_maximal_planar_graphs/experiments/md5_single_flip_preimage.py
+111
View File
@@ -0,0 +1,111 @@
"""Test the "single-edge-flip preimage" recipe for md5 triangulations.
For each md5 iso-class T at n:
1. For each face S = (a, b, c) of T:
For each edge e in {(a,b), (b,c), (a,c)}:
Construct G = T with edge e flipped to its apex edge.
Run the algorithm on (G, S).
Check whether the algorithm's output equals T (label-exact).
Report success rate per iso-class.
"""
import sys, os
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import networkx as nx
from collections import defaultdict
from triangulation_gen_fast import enumerate_all_triangulations_fast
from level_cycles import get_all_faces
from simple_level_resolution_coverage import (
simple_level_resolutions, is_triangulation,
)
def is_md5(T):
return min(T.degree(v) for v in T.nodes()) >= 5
def single_flip(T, u, v):
"""Flip edge (u,v) in T, returning the flipped graph (or None if invalid)."""
if not T.has_edge(u, v):
return None
ip, emb = nx.check_planarity(T)
if not ip:
return None
f1 = emb.traverse_face(u, v)
f2 = emb.traverse_face(v, u)
if len(f1) != 3 or len(f2) != 3:
return None
w = next(x for x in f1 if x != u and x != v)
x = next(y for y in f2 if y != u and y != v)
if w == x or T.has_edge(w, x):
return None
G = T.copy()
G.remove_edge(u, v)
G.add_edge(w, x)
return G
def test_iso_class(T, n, idx):
"""Try the single-edge-flip recipe on every face-edge pair."""
T_edges = set(frozenset(e) for e in T.edges())
ip, emb = nx.check_planarity(T)
if not ip:
return 0, 0
faces = get_all_faces(emb)
triangle_faces = [f for f in faces if len(f) == 3]
attempts = 0
successes = 0
success_examples = []
for face in triangle_faces:
a, b, c = face
source_set = {a, b, c}
for (u, v) in [(a, b), (b, c), (a, c)]:
G = single_flip(T, u, v)
if G is None:
continue
attempts += 1
for Gp in simple_level_resolutions(G, source_set):
if not is_triangulation(Gp, n):
continue
Gp_edges = set(frozenset(e) for e in Gp.edges())
if Gp_edges == T_edges:
successes += 1
if len(success_examples) < 3:
success_examples.append({
'face': tuple(face),
'flip_edge': (u, v),
'source': sorted(source_set),
})
break
return attempts, successes, success_examples
def main(ns):
for n in ns:
print(f"\n=== n={n} ===")
if n >= 11:
isos = enumerate_all_triangulations_fast(n)
from triangulation_gen import enumerate_all_triangulations
if n < 11:
isos = enumerate_all_triangulations(n)
md5 = [(i, T) for i, T in enumerate(isos) if is_md5(T)]
print(f" {len(md5)} md5 iso-class(es)")
for idx, T in md5:
ds = sorted([T.degree(v) for v in T.nodes()], reverse=True)
result = test_iso_class(T, n, idx)
if len(result) == 3:
attempts, successes, examples = result
else:
attempts, successes = result
examples = []
print(f" iso[{idx}] ds={ds}:")
print(f" attempts={attempts}, successes={successes}")
if examples:
for ex in examples[:1]:
print(f" example: face={ex['face']}, "
f"flip={ex['flip_edge']}, source={ex['source']}")
if __name__ == "__main__":
ns = [int(x) for x in sys.argv[1:]] if len(sys.argv) > 1 else [12, 13]
main(ns)
papers/level_resolutions_of_maximal_planar_graphs/experiments/plot_G_for_T.py
+118
View File
@@ -0,0 +1,118 @@
"""Plot G (with face source {0, 1, 6} producing T iso[2] at n=7 via Def 2.4)
alongside T itself, to show the relationship."""
import sys, os
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import networkx as nx
import numpy as np
import matplotlib.pyplot as plt
from triangulation_gen import enumerate_all_triangulations
def main():
n = 7
target_idx = 2
isos = enumerate_all_triangulations(n)
T = isos[target_idx]
# Constructed G: source face {0, 1, 6}, stacked from vertex 0
G_edges = [
(0, 1), (1, 6), (0, 6), # source face
(0, 2), (1, 2), (2, 6), # 2 inside (0, 1, 6)
(0, 3), (1, 3), (2, 3), # 3 inside (0, 1, 2)
(0, 4), (2, 4), (3, 4), # 4 inside (0, 2, 3)
(0, 5), (3, 5), (4, 5), # 5 inside (0, 3, 4)
]
G = nx.Graph(); G.add_edges_from(G_edges)
print(f"G edges: {sorted(G.edges())}")
print(f"G has {G.number_of_edges()} edges (need {3*n - 6})")
ip_g, emb_g = nx.check_planarity(G)
print(f"G planar: {ip_g}")
# BFS levels from {0, 1, 6}
from level_cycles import compute_levels
source = {0, 1, 6}
G_levels = compute_levels(G, source)
print(f"G BFS levels: {sorted(G_levels.items())}")
# Apply G's levels to T
even = [v for v in T.nodes() if G_levels[v] % 2 == 0]
odd = [v for v in T.nodes() if G_levels[v] % 2 == 1]
print(f"T even subgraph on {sorted(even)}: edges "
f"{sorted(T.subgraph(even).edges())}, "
f"bipartite: {nx.is_bipartite(T.subgraph(even))}")
print(f"T odd subgraph on {sorted(odd)}: edges "
f"{sorted(T.subgraph(odd).edges())}, "
f"bipartite: {nx.is_bipartite(T.subgraph(odd))}")
# Edges in G but not T, and vice versa
Ge = set(frozenset(e) for e in G.edges())
Te = set(frozenset(e) for e in T.edges())
only_G = Ge - Te
only_T = Te - Ge
print(f"Edges only in G: {sorted(only_G)}")
print(f"Edges only in T: {sorted(only_T)}")
# Use the face-area-balanced planar layout from balanced_layout.py.
from balanced_layout import balanced_planar_layout
outer_face = (0, 1, 6)
pos = balanced_planar_layout(G, outer_face, n_explore=4000, n_refine=2000)
fig, axes = plt.subplots(1, 2, figsize=(15, 7))
level_color = {0: '#3b82f6', 1: '#f59e0b'}
def draw(ax, graph, title, highlight_edges=None, missing_edges=None):
# Edges of this graph
for u, v in graph.edges():
if highlight_edges and frozenset([u, v]) in highlight_edges:
ax.plot([pos[u][0], pos[v][0]], [pos[u][1], pos[v][1]],
color='#22c55e', linewidth=3.5, zorder=2,
linestyle='-')
else:
ax.plot([pos[u][0], pos[v][0]], [pos[u][1], pos[v][1]],
color='#444', linewidth=1.5, zorder=2)
# Show missing edges as faint dashed
if missing_edges:
for (u, v) in missing_edges:
ax.plot([pos[u][0], pos[v][0]], [pos[u][1], pos[v][1]],
color='#ef4444', linewidth=1.5, zorder=1.5,
linestyle=':', alpha=0.5)
# Vertices colored by G-level
for v in graph.nodes():
ax.scatter(pos[v][0], pos[v][1],
c=level_color[G_levels[v]], s=900,
edgecolors='black', linewidths=2.0, zorder=3)
ax.text(pos[v][0], pos[v][1],
f"{v}\n$L_{{{G_levels[v]}}}$",
fontsize=12, ha='center', va='center',
fontweight='bold', zorder=4)
ax.set_title(title, fontsize=12)
ax.set_aspect('equal'); ax.axis('off')
draw(axes[0], G,
f"$G$: triangulation with face source $S = \\{{0, 1, 6\\}}$\n"
f"Green = edges that are in $G$ but not in $T$",
highlight_edges=only_G,
missing_edges=only_T)
draw(axes[1], T,
f"$T$: the target (iso[2] at $n = 7$). G-levels applied.\n"
f"Even subgraph bipartite: True; odd subgraph bipartite: True\n"
f"(Red dotted = edges in $T$ but not $G$.)",
missing_edges=only_G)
plt.suptitle(
"$T$ as a level resolution of $G$ (Def 2.4) — partition cardinality "
"$(|L_0|, |L_1|) = (3, 4)$.\n"
"Both parity subgraphs of $T$ under $G$'s levels are bipartite. "
"The algorithm of \\S5 does not produce $T$ from $(G, S)$, however.",
fontsize=12, y=1.02
)
plt.tight_layout()
out = os.path.join(os.path.dirname(os.path.abspath(__file__)),
'..', f'G_for_T_n{n}_idx{target_idx}.png')
plt.savefig(out, dpi=130, bbox_inches='tight')
print(f"saved: {out}")
if __name__ == "__main__":
main()
papers/level_resolutions_of_maximal_planar_graphs/experiments/plot_missing_iso.py
+161
View File
@@ -0,0 +1,161 @@
"""Plot a missing iso-class (not reachable as a simple level resolution)
with its BFS levels from a face source highlighted, to show why it cannot
be a simple level resolution."""
import sys, os
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import networkx as nx
import numpy as np
import matplotlib.pyplot as plt
from collections import defaultdict
from triangulation_gen import enumerate_all_triangulations
from level_cycles import compute_levels, level_sources, get_all_faces
def main():
n, target_idx = 7, 2
isos = enumerate_all_triangulations(n)
T = isos[target_idx]
print(f"iso[{target_idx}] at n={n}:")
print(f" edges: {sorted(T.edges())}")
ds = sorted([T.degree(v) for v in T.nodes()], reverse=True)
print(f" degree seq: {ds}")
ip, emb = nx.check_planarity(T)
# Try every face source and check if T is self-resolution from that source
faces = get_all_faces(emb)
triangle_faces = [f for f in faces if len(f) == 3]
print(f" triangle faces: {triangle_faces}")
# Pick a face source for visualization (e.g., the first one)
source_face = triangle_faces[0]
source_set = set(source_face)
levels = compute_levels(T, source_set)
print(f" source face: {source_face}")
print(f" levels: {dict(sorted(levels.items()))}")
# Compute parity subgraph status
even_nodes = [v for v in T.nodes() if levels.get(v, 0) % 2 == 0]
odd_nodes = [v for v in T.nodes() if levels.get(v, 0) % 2 == 1]
even_sub = T.subgraph(even_nodes)
odd_sub = T.subgraph(odd_nodes)
print(f" even-level vertices: {sorted(even_nodes)}")
print(f" odd-level vertices: {sorted(odd_nodes)}")
print(f" even subgraph bipartite: {nx.is_bipartite(even_sub)}")
print(f" odd subgraph bipartite: {nx.is_bipartite(odd_sub)}")
pos = nx.planar_layout(T)
# Rotate/scale so source face is on the outside.
src_pts = np.array([pos[v] for v in source_face])
centroid = np.mean(list(pos.values()), axis=0)
for v in pos:
pos[v] = (pos[v] - centroid) * 1.5
fig, axes = plt.subplots(1, 3, figsize=(18, 6))
# Color vertices by level
level_colors = ['#3b82f6', '#f59e0b', '#10b981', '#ef4444', '#8b5cf6']
def draw_subgraph_panel(ax, subset_nodes, title, hilite_edges=None):
node_colors = [level_colors[levels[v] % len(level_colors)]
for v in T.nodes()]
# Draw all edges in light gray
nx.draw_networkx_edges(T, pos, ax=ax, edge_color='#cbd5e1', width=1.0,
alpha=0.6)
# Draw subset-induced edges in dark
sub = T.subgraph(subset_nodes)
nx.draw_networkx_edges(sub, pos, ax=ax, edge_color='#1f2937',
width=2.5)
# Highlight any odd cycles
if hilite_edges:
for (u, v) in hilite_edges:
ax.plot([pos[u][0], pos[v][0]], [pos[u][1], pos[v][1]],
color='#ef4444', linewidth=4.0, zorder=2,
alpha=0.85)
# Draw vertices
node_alpha = [1.0 if v in subset_nodes else 0.25 for v in T.nodes()]
for v in T.nodes():
color = node_colors[list(T.nodes()).index(v)]
a = 1.0 if v in subset_nodes else 0.25
ax.scatter(pos[v][0], pos[v][1], c=color, s=550,
edgecolors='black', linewidths=1.2, zorder=3,
alpha=a)
ax.text(pos[v][0], pos[v][1], f"{v}\nL{levels[v]}",
fontsize=10, ha='center', va='center',
fontweight='bold', zorder=4,
alpha=a)
ax.set_title(title, fontsize=11)
ax.set_aspect('equal')
ax.axis('off')
ax.set_xlim(-1.3, 1.3)
ax.set_ylim(-1.3, 1.3)
# Panel 1: full graph with source face highlighted
src_pos = [pos[v] for v in source_face]
poly = plt.Polygon(src_pos, color='#fef3c7', alpha=0.7, zorder=0.5)
axes[0].add_patch(poly)
draw_subgraph_panel(
axes[0], set(T.nodes()),
f"Full graph $T$ with face source $S = \\{{{','.join(map(str, sorted(source_face)))}\\}}$"
)
axes[0].set_title(
f"Full graph $T$ with face source $S = \\{{{','.join(map(str, sorted(source_face)))}\\}}$\n"
f"Yellow = source face (level 0)",
fontsize=11
)
# Panel 2: even-parity subgraph
even_edges = [(u, v) for u, v in even_sub.edges()]
# Find odd cycle in even subgraph
odd_cycle_even = None
try:
odd_cycle_even = nx.find_cycle(even_sub, orientation='ignore')
# Filter only odd cycles
if odd_cycle_even and len(odd_cycle_even) % 2 == 0:
odd_cycle_even = None
except nx.NetworkXNoCycle:
odd_cycle_even = None
hilite_e = [(u, v) for u, v, *_ in odd_cycle_even] if odd_cycle_even else None
draw_subgraph_panel(
axes[1], set(even_nodes),
f"Even-parity subgraph $E_{{T,S}}(T)$\n"
f"Vertices: $\\{{{','.join(map(str, sorted(even_nodes)))}\\}}$ "
f"(L0 $\\cup$ L2 $\\cup\\ldots$)\n"
f"Bipartite: {nx.is_bipartite(even_sub)} "
f"{'(odd cycle highlighted)' if hilite_e else ''}",
hilite_edges=hilite_e
)
# Panel 3: odd-parity subgraph
odd_cycle_odd = None
try:
odd_cycle_odd = nx.find_cycle(odd_sub, orientation='ignore')
if odd_cycle_odd and len(odd_cycle_odd) % 2 == 0:
odd_cycle_odd = None
except nx.NetworkXNoCycle:
odd_cycle_odd = None
hilite_o = [(u, v) for u, v, *_ in odd_cycle_odd] if odd_cycle_odd else None
draw_subgraph_panel(
axes[2], set(odd_nodes),
f"Odd-parity subgraph $O_{{T,S}}(T)$\n"
f"Vertices: $\\{{{','.join(map(str, sorted(odd_nodes)))}\\}}$ "
f"(L1 $\\cup$ L3 $\\cup\\ldots$)\n"
f"Bipartite: {nx.is_bipartite(odd_sub)} "
f"{'(odd cycle highlighted)' if hilite_o else ''}",
hilite_edges=hilite_o
)
plt.suptitle(
f"$n = {n}$ iso[{target_idx}]: a triangulation that is NOT reached as a simple level resolution.\n"
f"From any face source the source-face triangle creates an odd cycle in the even-parity subgraph; "
f"the algorithm of \\S5 cannot remove it without destroying other structure.",
fontsize=12, y=1.02
)
plt.tight_layout()
out = os.path.join(os.path.dirname(os.path.abspath(__file__)),
'..', f'missing_iso_n{n}_idx{target_idx}.png')
plt.savefig(out, dpi=130, bbox_inches='tight')
print(f"saved: {out}")
if __name__ == "__main__":
main()
papers/level_resolutions_of_maximal_planar_graphs/experiments/plot_missing_iso_4color.py
+71
View File
@@ -0,0 +1,71 @@
"""Plot the missing iso (n=7 iso[2]) with a proper 4-coloring."""
import sys, os
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import networkx as nx
import numpy as np
import matplotlib.pyplot as plt
from triangulation_gen import enumerate_all_triangulations
def main():
n, target_idx = 7, 2
isos = enumerate_all_triangulations(n)
T = isos[target_idx]
# 4-coloring
coloring = {0: 'A', 1: 'B', 2: 'C', 3: 'D',
4: 'D', 5: 'C', 6: 'B'}
color_to_hex = {'A': '#ef4444', 'B': '#3b82f6',
'C': '#22c55e', 'D': '#f59e0b'}
# Verify
for u, v in T.edges():
assert coloring[u] != coloring[v], f"Edge ({u},{v}) is monochromatic!"
print("4-coloring verified proper.")
# Layout: planar with source face on outside
pos = nx.planar_layout(T)
centroid = np.mean(list(pos.values()), axis=0)
for v in pos:
pos[v] = (pos[v] - centroid) * 1.5
fig, ax = plt.subplots(1, 1, figsize=(8, 8))
nx.draw_networkx_edges(T, pos, ax=ax, edge_color='#333', width=2.0)
for v in T.nodes():
ax.scatter(pos[v][0], pos[v][1],
c=color_to_hex[coloring[v]], s=900,
edgecolors='black', linewidths=2.0, zorder=3)
ax.text(pos[v][0], pos[v][1], f"{v}\n({coloring[v]})",
fontsize=12, ha='center', va='center',
fontweight='bold', zorder=4)
# Add a legend
from matplotlib.patches import Patch
legend_elements = [
Patch(facecolor=color_to_hex['A'], edgecolor='black',
label='A (1 vertex)'),
Patch(facecolor=color_to_hex['B'], edgecolor='black',
label='B (2 vertices)'),
Patch(facecolor=color_to_hex['C'], edgecolor='black',
label='C (2 vertices)'),
Patch(facecolor=color_to_hex['D'], edgecolor='black',
label='D (2 vertices)'),
]
ax.legend(handles=legend_elements, loc='upper right', fontsize=11)
ax.set_title(
f"Proper 4-coloring of $n = {n}$ iso[{target_idx}]\n"
f"Color cardinalities: $(|A|, |B|, |C|, |D|) = (1, 2, 2, 2)$.",
fontsize=13
)
ax.set_aspect('equal')
ax.axis('off')
out = os.path.join(os.path.dirname(os.path.abspath(__file__)),
'..', f'missing_iso_n{n}_idx{target_idx}_4color.png')
plt.savefig(out, dpi=130, bbox_inches='tight')
print(f"saved: {out}")
if __name__ == "__main__":
main()
papers/level_resolutions_of_maximal_planar_graphs/experiments/plot_missing_iso_levels.py
+113
View File
@@ -0,0 +1,113 @@
"""Plot iso[2] at n=7 with the depth labels that make it a level resolution
of some plane triangulation."""
import sys, os
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import networkx as nx
import numpy as np
import matplotlib.pyplot as plt
from triangulation_gen import enumerate_all_triangulations
def main():
n, target_idx = 7, 2
isos = enumerate_all_triangulations(n)
T = isos[target_idx]
# Witnessing partition (corresponds to a level resolution of some G)
levels = {0: 0, 1: 0, 6: 0, # L_0 = even
2: 1, 3: 1, 4: 1, 5: 1} # L_1 = odd
# Within-parity 2-colorings (the 4-coloring this induces)
within_color = {0: 'A', 1: 'B', 6: 'B',
2: 'C', 5: 'C', 3: 'D', 4: 'D'}
color_to_hex = {'A': '#ef4444', 'B': '#3b82f6',
'C': '#22c55e', 'D': '#f59e0b'}
# Sanity checks
even_nodes = [v for v in T.nodes() if levels[v] == 0]
odd_nodes = [v for v in T.nodes() if levels[v] == 1]
even_sub = T.subgraph(even_nodes)
odd_sub = T.subgraph(odd_nodes)
print(f"L_0 = {sorted(even_nodes)} edges: {sorted(even_sub.edges())} "
f"bipartite: {nx.is_bipartite(even_sub)}")
print(f"L_1 = {sorted(odd_nodes)} edges: {sorted(odd_sub.edges())} "
f"bipartite: {nx.is_bipartite(odd_sub)}")
# Verify 4-coloring
for u, v in T.edges():
assert within_color[u] != within_color[v], \
f"{u}({within_color[u]})-{v}({within_color[v]})"
print("4-coloring proper.")
pos = nx.planar_layout(T)
centroid = np.mean(list(pos.values()), axis=0)
for v in pos:
pos[v] = (pos[v] - centroid) * 1.5
fig, axes = plt.subplots(1, 2, figsize=(14, 7))
# Panel 1: Level labels (L_0 and L_1)
ax = axes[0]
nx.draw_networkx_edges(T, pos, ax=ax, edge_color='#666', width=1.6)
level_color = {0: '#3b82f6', 1: '#f59e0b'}
for v in T.nodes():
ax.scatter(pos[v][0], pos[v][1], c=level_color[levels[v]], s=900,
edgecolors='black', linewidths=2.0, zorder=3)
ax.text(pos[v][0], pos[v][1],
f"{v}\n$L_{{{levels[v]}}}$",
fontsize=12, ha='center', va='center',
fontweight='bold', zorder=4)
from matplotlib.patches import Patch
ax.legend(handles=[
Patch(facecolor=level_color[0], edgecolor='black',
label='$L_0 = \\{0, 1, 6\\}$ (even parity, source face of $G$)'),
Patch(facecolor=level_color[1], edgecolor='black',
label='$L_1 = \\{2, 3, 4, 5\\}$ (odd parity)'),
], loc='upper right', fontsize=10)
ax.set_title(
"Depth labels that make $T$ a level resolution\n"
"of some $G$ with face source $S = \\{0, 1, 6\\}$",
fontsize=12
)
ax.set_aspect('equal'); ax.axis('off')
# Panel 2: induced 4-coloring (refinement of levels)
ax = axes[1]
nx.draw_networkx_edges(T, pos, ax=ax, edge_color='#666', width=1.6)
for v in T.nodes():
ax.scatter(pos[v][0], pos[v][1],
c=color_to_hex[within_color[v]], s=900,
edgecolors='black', linewidths=2.0, zorder=3)
ax.text(pos[v][0], pos[v][1],
f"{v}\n({within_color[v]})",
fontsize=12, ha='center', va='center',
fontweight='bold', zorder=4)
ax.legend(handles=[
Patch(facecolor=color_to_hex['A'], edgecolor='black',
label='A: $\\{0\\}$ (red, $L_0$)'),
Patch(facecolor=color_to_hex['B'], edgecolor='black',
label='B: $\\{1, 6\\}$ (blue, $L_0$)'),
Patch(facecolor=color_to_hex['C'], edgecolor='black',
label='C: $\\{2, 5\\}$ (green, $L_1$)'),
Patch(facecolor=color_to_hex['D'], edgecolor='black',
label='D: $\\{3, 4\\}$ (orange, $L_1$)'),
], loc='upper right', fontsize=10)
ax.set_title(
"Induced proper 4-coloring (2-coloring within each parity).\n"
"Card. $(1, 2, 2, 2)$ grouped pairwise as $(3, 4) = (|L_0|, |L_1|)$.",
fontsize=12
)
ax.set_aspect('equal'); ax.axis('off')
plt.suptitle(
f"$n = 7$ iso[2] as a level resolution (Def 2.4): "
f"a partition exists, but the algorithm of \\S5 does not find it.",
fontsize=13, y=1.02
)
plt.tight_layout()
out = os.path.join(os.path.dirname(os.path.abspath(__file__)),
'..', f'missing_iso_n{n}_idx{target_idx}_levels.png')
plt.savefig(out, dpi=130, bbox_inches='tight')
print(f"saved: {out}")
if __name__ == "__main__":
main()
papers/level_resolutions_of_maximal_planar_graphs/experiments/simple_level_resolution_coverage.py
+22 -16
View File
@@ -374,11 +374,11 @@ def is_self_level_resolution(T):
def run(n):
isos = enumerate_all_triangulations(n)
print(f"n={n}: {len(isos)} iso-classes")
md4 = set()
md5 = set()
for i, T in enumerate(isos):
if min(T.degree(v) for v in T.nodes()) >= 4:
md4.add(i)
print(f" min-degree-4 iso-classes: {len(md4)}")
if min(T.degree(v) for v in T.nodes()) >= 5:
md5.add(i)
print(f" min-degree-5 iso-classes: {len(md5)}")
self_resolutions = set()
for i, T in enumerate(isos):
if is_self_level_resolution(T):
@@ -413,20 +413,26 @@ def run(n):
reached_any.add(tgt)
if is_bip:
reached_bip.add(tgt)
# Refined conjecture: every min-degree-4 iso-class is reached.
needed = md4 - self_resolutions
missing_any = sorted(needed - reached_any)
missing_bip = sorted(needed - reached_bip)
# Total iso-classes reached
all_iso = set(range(len(isos)))
total_any = len(reached_any)
total_bip = len(reached_bip)
missing_total_bip = sorted(all_iso - reached_bip)
print(f" (G, S) pairs: {total_pairs}")
print(f" triangulation outputs: {triangulation_outputs}")
print(f" bipartite-parity: {bipartite_outputs}")
print(f" needed (md4, not self): {len(needed)} iso-classes")
print(f" reached as any output: {len(reached_any & needed)} / {len(needed)}"
f" (missing: {missing_any[:10] if missing_any else 'none'}"
f"{'...' if len(missing_any) > 10 else ''})")
print(f" reached as bip-parity: {len(reached_bip & needed)} / {len(needed)}"
f" (missing: {missing_bip[:10] if missing_bip else 'none'}"
f"{'...' if len(missing_bip) > 10 else ''})")
print(f" bipartite-parity outputs:{bipartite_outputs}")
print(f" TOTAL ISO-CLASSES REACHED:")
print(f" any-output: {total_any} / {len(isos)}")
print(f" bipartite-parity: {total_bip} / {len(isos)}"
f" (missing: {missing_total_bip[:10] if missing_total_bip else 'none'}"
f"{'...' if len(missing_total_bip) > 10 else ''})")
# md5 subset
needed_md5 = md5 - self_resolutions
missing_md5 = sorted(needed_md5 - reached_bip)
print(f" md5 SUBSET (needed for Conjecture~5.7):")
print(f" needed: {len(needed_md5)}; reached bip: "
f"{len(reached_bip & needed_md5)} / {len(needed_md5)}"
f" (missing: {missing_md5[:10] if missing_md5 else 'none'})")
if __name__ == "__main__":
papers/level_resolutions_of_maximal_planar_graphs/experiments/test_cross_level_inverse.py
+110
View File
@@ -0,0 +1,110 @@
"""Test the conjecture: if T = algorithm(G, S), then G and T differ only
in cross-level edges (with respect to G's BFS levels from S).
If true, then flipping the cross-level edges of T (back to their apex pairs)
recovers G. This would give a constructive inverse procedure.
For various (G, S) pairs, run the algorithm to get T, then check:
(1) Are all edges in T \ G cross-level (endpoints at different G-levels)?
(2) Are all edges in G \ T cross-level?
"""
import sys, os
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import networkx as nx
from collections import defaultdict
from triangulation_gen import enumerate_all_triangulations
from triangulation_gen_fast import enumerate_all_triangulations_fast
from level_cycles import compute_levels, level_sources
from simple_level_resolution_coverage import (
simple_level_resolutions, is_triangulation,
)
def is_md5(T):
return min(T.degree(v) for v in T.nodes()) >= 5
def edges_summary(G, T, levels):
"""Compute edges only in G, only in T, and check cross-level status
based on G-levels."""
G_edges = set(frozenset(e) for e in G.edges())
T_edges = set(frozenset(e) for e in T.edges())
only_in_G = G_edges - T_edges
only_in_T = T_edges - G_edges
def is_cross_level(e):
u, v = tuple(e)
return levels.get(u, -1) != levels.get(v, -1)
in_G_cross = sum(1 for e in only_in_G if is_cross_level(e))
in_G_same = len(only_in_G) - in_G_cross
in_T_cross = sum(1 for e in only_in_T if is_cross_level(e))
in_T_same = len(only_in_T) - in_T_cross
# Also categorize by level diff
def level_diff(e):
u, v = tuple(e)
return abs(levels.get(u, -1) - levels.get(v, -1))
G_diffs = sorted([level_diff(e) for e in only_in_G])
T_diffs = sorted([level_diff(e) for e in only_in_T])
return {
'only_in_G': len(only_in_G),
'only_in_T': len(only_in_T),
'in_G_cross_level': in_G_cross,
'in_G_same_level': in_G_same,
'in_T_cross_level': in_T_cross,
'in_T_same_level': in_T_same,
'G_diffs': G_diffs,
'T_diffs': T_diffs,
}
def run_test(n, max_iso=20):
if n >= 11:
isos = enumerate_all_triangulations_fast(n)
else:
isos = enumerate_all_triangulations(n)
print(f"\n=== n={n} ({len(isos)} iso-classes) ===")
total = 0
all_cross = 0
some_same = 0
examples_with_same = []
for idx, G in enumerate(isos[:max_iso] if max_iso else isos):
ip, emb = nx.check_planarity(G)
if not ip:
continue
for kind, lab, source_set in level_sources(G, emb):
levels = compute_levels(G, source_set)
count = 0
for Gp in simple_level_resolutions(G, source_set):
count += 1
if count > 8:
break
if not is_triangulation(Gp, n):
continue
summary = edges_summary(G, Gp, levels)
total += 1
if summary['in_G_same_level'] == 0 and \
summary['in_T_same_level'] == 0:
all_cross += 1
else:
some_same += 1
if len(examples_with_same) < 3:
examples_with_same.append({
'iso': idx,
'source': (kind, lab),
**summary,
})
print(f" total (G, S, choice) triples tested: {total}")
print(f" all symdiff edges cross-level: {all_cross}")
print(f" some same-level: {some_same}")
if examples_with_same:
print(f" examples with same-level edges (first {len(examples_with_same)}):")
for ex in examples_with_same:
print(f" iso={ex['iso']} src={ex['source']}: "
f"|symdiff|={ex['only_in_G']}+{ex['only_in_T']}, "
f"same-level G={ex['in_G_same_level']}/T={ex['in_T_same_level']}, "
f"level diffs G={ex['G_diffs']}, T={ex['T_diffs']}")
if __name__ == "__main__":
ns = [int(x) for x in sys.argv[1:]] if len(sys.argv) > 1 else [7, 8, 9]
for n in ns:
run_test(n, max_iso=30)
papers/level_resolutions_of_maximal_planar_graphs/experiments/test_cross_level_iso_inverse.py
+135
View File
@@ -0,0 +1,135 @@
"""Test the user's revised conjecture:
For T = algorithm(G, S), there exists a cross-level edge Z in T
(other than the edges introduced by the algorithm) such that flipping Z
in T gives a graph isomorphic to G.
For various (G, S, T) triples, enumerate cross-level edges of T,
flip each, and check whether the result is iso to G.
"""
import sys, os
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import networkx as nx
from collections import defaultdict
from triangulation_gen import enumerate_all_triangulations
from level_cycles import compute_levels, level_sources
from simple_level_resolution_coverage import (
simple_level_resolutions, is_triangulation,
)
def flip_edge(G, u, v):
"""Flip edge (u, v) in G. Return flipped graph or None if invalid."""
if not G.has_edge(u, v):
return None
ip, emb = nx.check_planarity(G)
if not ip:
return None
f1 = emb.traverse_face(u, v)
f2 = emb.traverse_face(v, u)
if len(f1) != 3 or len(f2) != 3:
return None
w = next(x for x in f1 if x != u and x != v)
x = next(y for y in f2 if y != u and y != v)
if w == x or G.has_edge(w, x):
return None
Gp = G.copy()
Gp.remove_edge(u, v)
Gp.add_edge(w, x)
return Gp
def apply_flips(G, edges_to_flip):
"""Apply a sequence of edge flips. Skip flips that are no longer valid
(e.g., after a previous flip removed the edge)."""
Gc = G.copy()
applied = 0
for (u, v) in edges_to_flip:
Gp = flip_edge(Gc, u, v)
if Gp is None:
continue
Gc = Gp
applied += 1
return Gc, applied
def analyze(G, source_set, T, max_subset=6):
"""For T = algorithm(G, S), enumerate cross-level edges of T (w.r.t.
G-levels). Try all subsets up to size max_subset of the
cross-level edges that are INHERITED (i.e., not algorithm-introduced).
Check if any such subset, when flipped, gives a graph iso to G."""
from itertools import combinations
levels = compute_levels(G, source_set)
G_edges = set(frozenset(e) for e in G.edges())
T_edges = set(frozenset(e) for e in T.edges())
algorithm_added = T_edges - G_edges
cross_in_T = set()
for e in T_edges:
u, v = tuple(e)
if levels.get(u, -1) != levels.get(v, -1):
cross_in_T.add(e)
cross_inherited = cross_in_T - algorithm_added
# Try subsets of cross_inherited from size 1 up to max_subset
success_subsets = []
for k in range(1, min(max_subset, len(cross_inherited)) + 1):
for subset in combinations(cross_inherited, k):
edge_list = [tuple(e) for e in subset]
T_flipped, _ = apply_flips(T, edge_list)
if nx.is_isomorphic(T_flipped, G):
success_subsets.append(subset)
break # first one at this size is enough
if success_subsets:
break # found at smallest size
return {
'algorithm_added': len(algorithm_added),
'cross_inherited': len(cross_inherited),
'success_subset_size': len(success_subsets[0]) if success_subsets else None,
'has_iso_recovery': bool(success_subsets),
}
def run(n, max_per_iso=4):
isos = enumerate_all_triangulations(n)
print(f"\n=== n={n} ({len(isos)} iso-classes) ===")
summaries = []
for src_idx, G in enumerate(isos):
ip, emb = nx.check_planarity(G)
if not ip:
continue
for kind, lab, source_set in level_sources(G, emb):
count = 0
for Gp in simple_level_resolutions(G, source_set):
count += 1
if count > max_per_iso:
break
if not is_triangulation(Gp, n):
continue
# Skip cases with no algorithm flips (G == Gp)
if set(frozenset(e) for e in Gp.edges()) == \
set(frozenset(e) for e in G.edges()):
continue
summary = analyze(G, source_set, Gp)
summaries.append({
'src': src_idx,
'source': (kind, lab),
**summary,
})
print(f" total (G, S, T) triples (with algorithm flips): {len(summaries)}")
recoverable = sum(1 for s in summaries if s['has_iso_recovery'])
print(f" triples where SOME inherited-cross-level subset recovers iso(G): "
f"{recoverable} / {len(summaries)}")
# Distribution of minimal subset size
size_dist = defaultdict(int)
for s in summaries:
size_dist[s['success_subset_size']] += 1
print(f" minimal subset size distribution: "
f"{dict(sorted((k, v) for k, v in size_dist.items() if k is not None))}")
failures = sum(1 for s in summaries if not s['has_iso_recovery'])
if failures:
print(f" {failures} triples with NO recovery (within max subset size)")
if __name__ == "__main__":
ns = [int(x) for x in sys.argv[1:]] if len(sys.argv) > 1 else [7, 8]
for n in ns:
run(n)
papers/level_resolutions_of_maximal_planar_graphs/paper.tex
+115 -158
View File
@@ -38,6 +38,7 @@
\usepackage{hyperref}
\usepackage{enumitem}
\usepackage{graphicx}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
@@ -91,7 +92,7 @@ structural foundation of this approach is that each level subgraph $L_k$
of $G$ is outerplanar, and outerplanar graphs are 3-chromatic; the level-resolution
problem is precisely to flip edges of $G$ to reduce each $L_k$ from
chromatic number $3$ to $2$. We present computational results characterizing
which isomorphism classes of maximal planar graphs on $n = 6, \ldots, 11$
which isomorphism classes of maximal planar graphs on $n = 6, \ldots, 12$
vertices arise as level resolutions, and verify that every iso-class is
reachable at every tested size.
\end{abstract}
@@ -122,7 +123,7 @@ The remaining question is when level resolutions exist. We conjecture:
\item every plane triangulation $G'$ is a level resolution of some
plane triangulation $G$ via some level source; or, in a restricted
form,
\item every plane triangulation of minimum degree at least 4 is a level
\item every plane triangulation of minimum degree at least 5 is a level
resolution of some plane triangulation.
\end{enumerate}
@@ -266,14 +267,14 @@ the parity 2-coloring.
\section{Computational evidence}
We enumerated all non-isomorphic triangulations on $n \in \{6, \ldots, 11\}$
We enumerated all non-isomorphic triangulations on $n \in \{6, \ldots, 12\}$
via vertex insertion followed by edge-flip closure (see
\texttt{triangulation\_gen.py} and the faster
\texttt{triangulation\_gen\_fast.py} for $n \geq 11$). For each isomorphism
class, we computed the full set of iso-classes reachable as level
resolutions across all valid level sources.
\subsection{Coverage at $n = 6, \ldots, 11$}
\subsection{Coverage at $n = 6, \ldots, 12$}
Table~\ref{tab:coverage} lists the resolution behavior for each iso-class.
A class $T_i$ is \emph{covered} if it appears as the resolution iso-class of
@@ -291,6 +292,7 @@ $n$ & Iso-classes & Reachable as level resolutions \\
9 & 50 & all 50 \\
10 & 233 & all 233 \\
11 & 1249 & all 1249 \\
12 & 7595 & all 7595 \\
\hline
\end{tabular}
\caption{Iso-class coverage under the level-resolution definition.}
@@ -299,7 +301,7 @@ $n$ & Iso-classes & Reachable as level resolutions \\
\begin{observation}
\label{obs:preimage}
For every $n \in \{6, \ldots, 11\}$, every plane-triangulation iso-class on
For every $n \in \{6, \ldots, 12\}$, every plane-triangulation iso-class on
$n$ vertices is a level resolution of some plane triangulation on the same
vertex set.
\end{observation}
@@ -322,9 +324,9 @@ induced subgraphs.
\subsection{Surjectivity at $n = 12$: the icosahedron}
The icosahedron is the unique 5-regular triangulation on 12 vertices and a
natural test case at $n = 12$ since it has no degree-3 vertex (so the
$\mathrm{md}_4$ restriction is irrelevant) and high symmetry constrains the
achievable parity-cardinality splits to $(6, 6)$ from any source. We verify
natural test case at $n = 12$: it is the smallest minimum-degree-$5$
plane triangulation, and its high symmetry constrains the achievable
parity-cardinality splits to $(6, 6)$ from any source. We verify
directly that the icosahedron admits a bipartite 2-partition of cardinality
$(6, 6)$: with vertices labelled as in the standard icosahedral graph, the
partition $\{0, 1, 2, 3, 4, 7\} \mid \{5, 6, 8, 9, 10, 11\}$ has both
@@ -341,22 +343,26 @@ vertices.
\subsection{Restatement of the resolution-preimage conjecture}
In light of Observations~\ref{obs:preimage} and~\ref{obs:icosa}, we
restate Conjecture~\ref{conj:preimage} more confidently:
restate Conjecture~\ref{conj:preimage} in the form we will focus on
through the constructive sections that follow:
\begin{conjecture}[$\mathrm{md}_4$ surjectivity]
\label{conj:md4}
For every $n \geq 6$, every minimum-degree-4 plane triangulation on $n$
vertices is a level resolution of some plane triangulation on $n$ vertices.
\begin{conjecture}[$\mathrm{md}_5$ surjectivity]
\label{conj:md5}
For every $n \geq 12$, every minimum-degree-$5$ plane triangulation on $n$
vertices is a level resolution of some plane triangulation on $n$
vertices.
\end{conjecture}
By the equivalence noted in Section~3, this is equivalent to a $4$-coloring
statement: every minimum-degree-4 plane triangulation admits a proper
$4$-coloring whose color-class cardinalities, grouped pairwise, match some
BFS-level parity cardinality on the same vertex set. Since the
unrestricted preimage conjecture also appears to hold at every tested $n$,
the $\mathrm{md}_4$ restriction may be unnecessary; we retain it here as
the form most amenable to the constructive techniques explored in
Section~\ref{sec:flip-algorithm}.
statement: every minimum-degree-$5$ plane triangulation admits a proper
$4$-coloring whose color-class cardinalities, grouped pairwise, match
some BFS-level parity cardinality on the same vertex set. The
$\mathrm{md}_5$ restriction is the form most amenable to the constructive
techniques explored in Section~\ref{sec:flip-algorithm}; the unrestricted
preimage conjecture (Conjecture~\ref{conj:preimage}) appears to hold at
every tested $n$ as well, but $\mathrm{md}_5$ removes the degree-$3$ and
degree-$4$ vertices that obstruct several of the inductive structures
considered later.
\section{An edge-flip resolution algorithm}
\label{sec:flip-algorithm}
@@ -498,142 +504,89 @@ $(G, S, k)$ triples — $4645$ at $n \leq 10$ and $24995$ at $n = 11$ —
Phase~1 always terminates and Phase~2 always succeeds.
\end{observation}
\paragraph{Coverage test for Conjecture~\ref{conj:simple-md4}.} For each
$n \in \{6, \ldots, 11\}$ we enumerate all plane-triangulation iso-classes
on $n$ vertices. For each iso-class $G$, each level source $S$ of $G$,
and each branching choice within the algorithm — Phase~1 ties on which
deepest interior face and which lowest-depth neighbor to flip, Phase~2
choices of which outer-face edge to flip for each odd or even
outer-incident cycle (including the option to leave even cycles
untouched), and the option to skip the source-triangle break when $S$ is
a face — we run Phase~1 to termination and then Phase~2, recording the
algorithm's output $G'$ as a labelled simple graph. We check three
properties: (a) $G'$ is a triangulation (no multi-edge survived the
Phase~2 flips), (b) the parity subgraphs $E_{G, S}(G')$ and
$O_{G, S}(G')$ are both bipartite, and (c) the iso-class of $G'$.
Aggregating over all $(G, S, \text{branch-choices})$ triples yields the
set of iso-classes attainable as algorithm outputs satisfying (a)+(b);
we compare this set against the minimum-degree-$4$ iso-classes at each
$n$.
\paragraph{Coverage test.} For each $n$ we enumerate all
plane-triangulation iso-classes on $n$ vertices. For each iso-class $G$,
each level source $S$ of $G$, and each branching choice within the
algorithm — Phase~1 ties on which deepest interior face and which
lowest-depth neighbor to flip, Phase~2 choices of which outer-face edge
to flip for each odd or even outer-incident cycle (including the option
to leave even cycles untouched), and the option to skip the
source-triangle break when $S$ is a face — we run Phase~1 to termination
and then Phase~2, recording the algorithm's output $G'$ as a labelled
simple graph. We check three properties: (a) $G'$ is a triangulation (no
multi-edge survived the Phase~2 flips), (b) the parity subgraphs
$E_{G, S}(G')$ and $O_{G, S}(G')$ are both bipartite, and (c) the
iso-class of $G'$. Aggregating over all $(G, S, \text{branch-choices})$
triples yields the set of iso-classes attainable as algorithm outputs
satisfying (a)+(b); we compare this set against the
minimum-degree-$5$ iso-classes at each $n$.
Table~\ref{tab:simple-coverage} reports the empirical results of this
test for $n = 6, \ldots, 11$.
\begin{table}[h]
\centering
\begin{tabular}{rrll}
\hline
$n$ & Iso-classes & Algorithm output (any) & Simple level resolutions \\
\hline
6 & 2 & all 2 & all 2 \\
7 & 5 & all 5 & 4 of 5 \\
8 & 14 & all 14 & 12 of 14 \\
9 & 50 & all 50 & 49 of 50 \\
10 & 233 & 231 of 233 & 225 of 233 \\
11 & 1249 & 1247 of 1249 & 1232 of 1249 \\
\hline
\end{tabular}
\caption{Simple-resolution coverage under the algorithm of
Section~\ref{sec:flip-algorithm}. ``Algorithm output (any)'' counts
iso-classes that appear as the iso-class of some labelled triangulation
output of the algorithm; ``Simple level resolutions'' counts iso-classes
that additionally satisfy the bipartite-parity condition of
Definition~\ref{def:simple-level-resolution}.}
\label{tab:simple-coverage}
\end{table}
\begin{observation}
\label{obs:md4-simple-resolution}
For every $n \in \{6, 7, 8, 9, 10, 11\}$, every plane triangulation
iso-class on $n$ vertices with minimum degree at least $4$ is a simple
level resolution of some plane triangulation on $n$ vertices. Concretely,
the counts of minimum-degree-$4$ iso-classes — $1, 1, 2, 5, 12, 34$ at
$n = 6, \ldots, 11$ — are all reached by the algorithm with bipartite
parity subgraphs (Definition~\ref{def:simple-level-resolution}).
\label{obs:md5-simple-resolution}
At $n = 12$ the unique minimum-degree-$5$ plane triangulation is the
icosahedron. An exhaustive search over all $7595$ iso-classes at
$n = 12$, all level sources, and all algorithm branching choices found
zero non-degenerate $(G, S)$ pair such that the algorithm produces a
triangulation isomorphic to the icosahedron with bipartite parity
subgraphs. The icosahedron is nonetheless a level resolution in the
sense of Definition~\ref{def:resolution} (Observation~\ref{obs:icosa}
and Table~\ref{tab:coverage}); the empirical evidence indicates that
it is \emph{not} a simple level resolution under the algorithm of
Section~\ref{sec:flip-algorithm}.
\end{observation}
\begin{conjecture}[Simple-resolution $\mathrm{md}_4$ surjectivity]
\label{conj:simple-md4}
For every $n \geq 6$, every minimum-degree-$4$ plane triangulation on $n$
vertices is a simple level resolution of some plane triangulation on $n$
vertices.
\end{conjecture}
The negative result of Observation~\ref{obs:md5-simple-resolution}
refutes the naive surjectivity statement that every md$_5$
triangulation is a simple level resolution; even the smallest example
fails. Figure~\ref{fig:missing-iso} illustrates the analogous
obstruction at $n = 7$: the simplest missing iso-class. In both cases
the source-face triangle of a face source forces an odd cycle in the
even-parity subgraph, and a parallel small odd cycle appears in the
odd-parity subgraph, so no choice of source $S$ makes the target $T$
its own level resolution; meanwhile no $(G, S)$ with $G \neq T$
produces $T$ under the algorithm either.
The minimum-degree-$4$ restriction in Conjecture~\ref{conj:simple-md4} is
necessary: at $n = 8$, the unique iso-class with three degree-$3$
vertices is not reachable by the algorithm; at $n = 10$, two further
iso-classes with four degree-$3$ vertices and high-degree hubs fail to
appear among algorithm outputs.
\subsection{Towards a proof: a contraction--lift strategy}
\label{sec:contraction-lift}
We sketch an inductive strategy for Conjecture~\ref{conj:simple-md4}
that we have verified empirically at small $n$ and offer here as a
roadmap for further work.
Let $T$ be a plane triangulation with minimum degree at least $4$, and
let $v \in V(T)$ be a degree-$4$ vertex with cyclic neighbors
$a, b, c, d$ (in the cyclic order inherited from $T$'s planar
embedding). Removing $v$ from $T$ exposes the $4$-cycle $abcd$, which we
retriangulate by adding one of the two diagonals $(a, c)$ or $(b, d)$.
We call this operation \emph{contraction at $v$ along diagonal
$(a, c)$}, denoted $T_{v, (a, c)}$. The contraction is \emph{valid} when
the chosen diagonal is not already an edge of $T$.
\begin{lemma}[Good contraction]
\label{lem:good-contraction}
Let $T$ be a plane triangulation on $n \geq 7$ vertices with minimum
degree at least $4$. Then there exist a degree-$4$ vertex $v \in V(T)$,
with cyclic neighbors $a, b, c, d$, and an unordered pair
$\{a, c\}$ such that:
\begin{enumerate}
\item $(a, c) \not\in E(T)$;
\item $\deg_T(b) \geq 5$ and $\deg_T(d) \geq 5$.
\end{enumerate}
Under these conditions $T_{v, (a, c)}$ is a plane triangulation on
$n - 1$ vertices with minimum degree at least $4$.
\end{lemma}
The conditions of Lemma~\ref{lem:good-contraction} ensure that the
contraction is valid (1) and md$_4$-preserving (2): the only vertices
whose degree changes under $T \to T_{v, (a, c)}$ are $a, b, c, d$, with
$\deg(a)$ and $\deg(c)$ unchanged (each loses the edge to $v$ but gains
the edge from the diagonal), while $\deg(b)$ and $\deg(d)$ each decrease
by $1$.
The lemma is empirically true at $n = 7, \ldots, 11$ for every md$_4$
iso-class; we conjecture it holds for all $n \geq 7$. The $n = 6$ case
is excluded: the unique md$_4$ iso-class is the octahedron, in which
every vertex has all four cyclic neighbors at degree $4$ and so no
contraction preserves md$_4$. The octahedron is therefore the base case
of the proposed induction.
\begin{lemma}[Lift]
\label{lem:lift}
Let $T$ be a plane triangulation with minimum degree at least $4$, and
suppose Lemma~\ref{lem:good-contraction} applies via vertex $v$ and
diagonal $(a, c)$ with $T_{v, (a, c)}$ the resulting contraction. Let
$H$ be a plane triangulation on $V(T_{v, (a, c)}) = V(T) \setminus \{v\}$
and $S$ a level source of $H$ such that the algorithm of
Section~\ref{sec:flip-algorithm} applied to $(H, S)$ produces
$T_{v, (a, c)}$ as a labelled simple graph. Define the \emph{lift}
$G \;:=\; H[a, b, c, d, v]$ by:
\begin{itemize}
\item adding vertex $v$ to $V(H)$;
\item removing the edge $(a, c)$ from $E(H)$;
\item adding the four edges $(v, a), (v, b), (v, c), (v, d)$.
\end{itemize}
Then $G$ is a plane triangulation on $|V(T)|$ vertices, and the
algorithm of Section~\ref{sec:flip-algorithm} applied to $(G, S)$
produces $T$.
\end{lemma}
Lemma~\ref{lem:lift} requires that $(a, c) \in E(H)$ and that the two
triangles of $H$ bordering $(a, c)$ have boundary
$\{a, b, c, d\}$. When these conditions hold, the lift restores a
degree-$4$ vertex $v$ inserted into the quadrilateral $abcd$; when they
fail, the lift is undefined and a different labelled preimage $H$ must
be chosen.
\paragraph{Inductive scheme.}
Conjecture~\ref{conj:simple-md4} would follow from
Lemmas~\ref{lem:good-contraction} and~\ref{lem:lift} together with the
existence at each step of a labelled preimage $H$ satisfying the lift's
side conditions. The base case is the octahedron at $n = 6$, which is
empirically a simple level resolution
(Observation~\ref{obs:md4-simple-resolution}). The inductive step takes
an md$_4$ target $T$ on $n$ vertices, applies
Lemma~\ref{lem:good-contraction} to obtain an md$_4$ contraction
$T_{v, (a, c)}$ on $n - 1$ vertices, invokes the inductive hypothesis to
produce a labelled preimage $H$, and applies Lemma~\ref{lem:lift} to
lift $H$ to $G$ with $\mathrm{alg}(G, S) = T$.
We have verified the entire scheme by hand for the unique md$_4$
iso-class at $n = 7$: contraction at $v = 2$ along diagonal $(4, 3)$
yields the octahedron on six vertices labelled $\{0, 1, 3, 4, 5, 6\}$;
a labelled preimage $H$ exists with source $S = \{0, 1, 6\}$; lifting
along $(4, 3, v = 2)$ produces a triangulation $G$ on seven vertices on
which the algorithm with source $S$ recovers $T$ exactly. The principal
remaining work is a proof of Lemma~\ref{lem:good-contraction} for all
$n \geq 7$, a proof of Lemma~\ref{lem:lift} (which involves analysing
how the algorithm's depth-guided flips interact with the added vertex
$v$), and a guarantee that a label-faithful preimage $H$ always
exists.
\begin{figure}
\centering
\includegraphics[width=\textwidth]{missing_iso_n7_idx2.png}
\caption{At $n = 7$, iso-class $T$ with degree sequence
$(6, 5, 5, 5, 3, 3, 3)$ is not a simple level resolution. Left:
$T$ drawn with face source $S = \{0, 1, 5\}$ outlined; vertices are
labelled by their BFS level. Middle: the even-parity subgraph
$E_{T,S}(T)$, induced on $\{0, 1, 5\}$, contains the source-face
triangle (highlighted) — an odd cycle. Right: the odd-parity subgraph
$O_{T,S}(T)$, induced on $\{2, 3, 4, 6\}$, contains a triangle on
$\{2, 3, 6\}$ (highlighted). The obstruction is identical for every
face source of $T$; vertex sources at degree-$3$ vertices produce
$L_1$ triangles in the odd-parity subgraph.}
\label{fig:missing-iso}
\end{figure}
\begin{question}
\label{q:terminate-all-n}
@@ -648,9 +601,10 @@ The computational results suggest the following:
\begin{enumerate}
\item Conjecture~\ref{conj:preimage} (resolution preimage) holds at every
tested size: all iso-classes on $n \in \{6, \ldots, 11\}$ vertices
arise as level resolutions, and the icosahedron does at $n = 12$
(Observations~\ref{obs:preimage} and~\ref{obs:icosa}).
tested size: all iso-classes on $n \in \{6, \ldots, 12\}$ vertices
arise as level resolutions (Observation~\ref{obs:preimage}; the
$n = 12$ case includes the icosahedron, verified directly in
Observation~\ref{obs:icosa}).
\item Each level subgraph $L_k$ of $G$ is outerplanar
(Theorem~\ref{thm:outerplanar}), so each $L_k$ is 3-chromatic
classically and independently of 4CT. The level-resolution problem
@@ -678,10 +632,13 @@ accepting a multigraph if the apex edge already exists.
Observation~\ref{obs:empirical-lk-bipartite} records that the algorithm
terminates and succeeds at the level-bipartiteness layer on all $29640$
tested $(G, S, k)$ triples at $n \in \{9, 10, 11\}$.
Observation~\ref{obs:md4-simple-resolution} records that every
minimum-degree-$4$ iso-class on $n \leq 11$ vertices is reached as a
simple level resolution; Conjecture~\ref{conj:simple-md4} extends this
to all $n$.
Observation~\ref{obs:md5-simple-resolution} records that the
icosahedron is empirically \emph{not} a simple level resolution under
the algorithm; the naive minimum-degree-$5$ surjectivity statement
therefore fails at the first md$_5$ case. Table~\ref{tab:simple-coverage}
shows that the gap appears already at $n = 7$ with one missing
iso-class, growing to $17$ missing at $n = 11$; Figure~\ref{fig:missing-iso}
illustrates the structural obstruction.
Question~\ref{q:terminate-all-n} asks whether Phase~1 terminates in
general.