diff --git a/papers/dual_decomposition_minimal_counterexamples/experiments/check_all_distinct_exists.py b/papers/dual_decomposition_minimal_counterexamples/experiments/check_all_distinct_exists.py new file mode 100644 index 0000000..1677684 --- /dev/null +++ b/papers/dual_decomposition_minimal_counterexamples/experiments/check_all_distinct_exists.py @@ -0,0 +1,329 @@ +"""Probe: even when phi_t* is in a Kempe class with no all-distinct, does +H_t* itself admit an all-distinct coloring in SOME (other) Kempe class? + +Reuses the Conj 3.6 counterexample: n=14, tri#1, i_red=0, phi_1 from the +chord-apex+Kempe colorings. Enumerates every proper 3-edge-coloring of +H_t*, marks the Kempe classes, and for each class reports whether it +contains an all-distinct coloring. + +Run with: sage experiments/check_all_distinct_exists.py +""" +from sage.all import Graph +from sage.graphs.graph_generators import graphs +import sys + + +def dual_of(G): + G.is_planar(set_embedding=True) + faces = G.faces() + edge_to_faces = {} + for fi, face in enumerate(faces): + for u, v in face: + edge_to_faces.setdefault(frozenset((u, v)), []).append(fi) + dual_edges = [(fs[0], fs[1]) for fs in edge_to_faces.values() if len(fs) == 2] + return Graph(dual_edges, multiedges=False, loops=False) + + +def proper_3_edge_colorings(G): + edges = list(G.edges(labels=False)) + n = len(edges) + adj = [[] for _ in range(n)] + for i in range(n): + u, v = edges[i][0], edges[i][1] + for j in range(i): + x, y = edges[j][0], edges[j][1] + if u in (x, y) or v in (x, y): + adj[i].append(j) + adj[j].append(i) + coloring = [-1] * n + results = [] + + def back(k): + if k == n: + results.append(tuple(coloring)) + return + for c in range(3): + if all(coloring[j] != c for j in adj[k]): + coloring[k] = c + back(k + 1) + coloring[k] = -1 + + back(0) + return edges, results + + +def kempe_cycle(edges, coloring, start_idx, color_pair): + a, b = color_pair + if coloring[start_idx] not in (a, b): + return set() + in_sub = set(i for i in range(len(edges)) if coloring[i] in (a, b)) + visited = {start_idx} + stack = [start_idx] + while stack: + cur = stack.pop() + u, v = edges[cur][0], edges[cur][1] + for j in in_sub: + if j in visited: + continue + x, y = edges[j][0], edges[j][1] + if u in (x, y) or v in (x, y): + visited.add(j) + stack.append(j) + return visited + + +def edge_idx(edges, e_frozen): + for i, e in enumerate(edges): + if frozenset((e[0], e[1])) == e_frozen: + return i + return None + + +def matches_chord_apex_kempe(edges, col, named): + idx = {role: edge_idx(edges, ns) for role, ns in named.items()} + if any(v is None for v in idx.values()): + return False + c_spike = col[idx['spike']] + c_merged = col[idx['merged']] + if c_spike != c_merged: + return False + c_s0 = col[idx['side_0']] + c_s1 = col[idx['side_1']] + kc0 = kempe_cycle(edges, col, idx['spike'], (c_spike, c_s0)) + if idx['side_0'] not in kc0 or idx['merged'] not in kc0: + return False + kc1 = kempe_cycle(edges, col, idx['spike'], (c_spike, c_s1)) + if idx['side_1'] not in kc1 or idx['merged'] not in kc1: + return False + return True + + +def apply_reduction(G, face, i, v_n_label): + boundary = [u for (u, v) in face] + if len(set(boundary)) != 5: + return None + A = [] + for B_k in boundary: + outer = [w for w in G.neighbor_iterator(B_k) if w not in boundary] + if len(outer) != 1: + return None + A.append(outer[0]) + if len(set(A)) != 5: + return None + if A[(i + 3) % 5] == A[(i + 4) % 5]: + return None + H = G.copy() + for v in boundary: + H.delete_vertex(v) + H.add_vertex(v_n_label) + side_0 = (v_n_label, A[i]) + spike = (v_n_label, A[(i + 1) % 5]) + side_1 = (v_n_label, A[(i + 2) % 5]) + merged = (A[(i + 3) % 5], A[(i + 4) % 5]) + H.add_edges([side_0, spike, side_1, merged]) + if H.has_multiple_edges() or H.has_loops(): + return None + if not H.is_planar(set_embedding=True): + return None + if not all(H.degree(v) == 3 for v in H.vertex_iterator()): + return None + return { + 'H': H, 'A': A, + 'named': { + 'spike': frozenset(spike), + 'side_0': frozenset(side_0), + 'side_1': frozenset(side_1), + 'merged': frozenset(merged), + }, + } + + +def find_safe_pentagonal_face(G, protected): + for face in G.faces(): + if len(face) != 5: + continue + boundary = [u for (u, v) in face] + boundary_edges = [frozenset([u, v]) for (u, v) in face] + externals = [] + A = [] + ok = True + for B_k in boundary: + outer = [w for w in G.neighbor_iterator(B_k) if w not in boundary] + if len(outer) != 1: + ok = False + break + externals.append(frozenset([B_k, outer[0]])) + A.append(outer[0]) + if not ok: + continue + if any(e in protected for e in boundary_edges + externals): + continue + return boundary, externals, A + return None + + +def valid_index(f_vec, A): + for i in range(5): + if f_vec[(i + 3) % 5] != f_vec[(i + 4) % 5]: + continue + if len({f_vec[i], f_vec[(i + 1) % 5], f_vec[(i + 2) % 5]}) != 3: + continue + if A[(i + 3) % 5] == A[(i + 4) % 5]: + continue + return i + return None + + +def run_algorithm_to_completion(H, phi_1_dict, named_step1, vn_start=10000): + H = H.copy() + coloring = dict(phi_1_dict) + all_named = [named_step1] + E = set(named_step1.values()) + next_vn = vn_start + while True: + H.is_planar(set_embedding=True) + result = find_safe_pentagonal_face(H, E) + if result is None: + break + boundary, externals, A = result + f_vec = [coloring[e] for e in externals] + i_t = valid_index(f_vec, A) + if i_t is None: + break + v_n = next_vn + next_vn += 1 + H_new = H.copy() + for v in boundary: + H_new.delete_vertex(v) + H_new.add_vertex(v_n) + side_0 = (v_n, A[i_t]) + spike = (v_n, A[(i_t + 1) % 5]) + side_1 = (v_n, A[(i_t + 2) % 5]) + merged = (A[(i_t + 3) % 5], A[(i_t + 4) % 5]) + H_new.add_edges([side_0, spike, side_1, merged]) + if H_new.has_multiple_edges() or H_new.has_loops(): + break + if not H_new.is_planar(set_embedding=True): + break + H = H_new + coloring = {e: c for e, c in coloring.items() + if not any(u in boundary for u in e)} + coloring[frozenset(side_0)] = f_vec[i_t] + coloring[frozenset(spike)] = f_vec[(i_t + 1) % 5] + coloring[frozenset(side_1)] = f_vec[(i_t + 2) % 5] + coloring[frozenset(merged)] = f_vec[(i_t + 3) % 5] + named = { + 'spike': frozenset(spike), + 'side_0': frozenset(side_0), + 'side_1': frozenset(side_1), + 'merged': frozenset(merged), + } + E |= set(named.values()) + all_named.append(named) + return H, coloring, all_named + + +def is_all_distinct(edges, col, all_named): + for named in all_named: + i_s = edge_idx(edges, named['spike']) + i_m = edge_idx(edges, named['merged']) + if i_s is None or i_m is None: + return False + if col[i_s] == col[i_m]: + return False + return True + + +def main(): + print("Reconstructing Conj 3.6 counterexample: n=14, tri#1, i_red=0") + for G in graphs.triangulations(14, minimum_degree=5): + D = dual_of(G) + D.is_planar(set_embedding=True) + chosen = None + for face in D.faces(): + if len(face) != 5: + continue + res = apply_reduction(D, face, 0, 9999) + if res is None: + continue + H_1, named_1 = res['H'], res['named'] + edges_1, colorings_1 = proper_3_edge_colorings(H_1) + cand = [c for c in colorings_1 + if matches_chord_apex_kempe(edges_1, c, named_1)] + if cand: + chosen = (face, res, cand) + break + if chosen is None: + continue + face, res, cand = chosen + H_1, named_1 = res['H'], res['named'] + edges_1, _ = proper_3_edge_colorings(H_1) + if not cand: + continue + phi_1 = cand[0] + phi_1_dict = {frozenset((e[0], e[1])): c for e, c in zip(edges_1, phi_1)} + H_final, phi_final_dict, all_named = run_algorithm_to_completion( + H_1, phi_1_dict, named_1) + edges_f, colorings_f = proper_3_edge_colorings(H_final) + print(f" H_t*: |V|={H_final.order()}, |E|={H_final.size()}, " + f"{len(colorings_f)} proper 3-edge-colorings, " + f"{len(all_named)} named-edge steps.") + + # Kempe equivalence classes via union-find + col_idx = {c: i for i, c in enumerate(colorings_f)} + parent = list(range(len(colorings_f))) + + def find(x): + while parent[x] != x: + parent[x] = parent[parent[x]] + x = parent[x] + return x + + def union(x, y): + rx, ry = find(x), find(y) + if rx != ry: + parent[rx] = ry + + for c_idx, col in enumerate(colorings_f): + for pair in [(0, 1), (0, 2), (1, 2)]: + visited = set() + for start in range(len(edges_f)): + if col[start] not in pair or start in visited: + continue + cyc = kempe_cycle(edges_f, col, start, pair) + visited |= cyc + a, b = pair + new_col = list(col) + for k in cyc: + if new_col[k] == a: + new_col[k] = b + elif new_col[k] == b: + new_col[k] = a + new_col = tuple(new_col) + if new_col != col and new_col in col_idx: + union(c_idx, col_idx[new_col]) + + roots = {} + for i in range(len(colorings_f)): + r = find(i) + roots.setdefault(r, []).append(i) + + # phi_t* identification + phi_final = tuple(phi_final_dict[frozenset((e[0], e[1]))] + for e in edges_f) + phi_idx = colorings_f.index(phi_final) + phi_root = find(phi_idx) + + print() + print(f" Found {len(roots)} Kempe equivalence classes:") + for r, members in sorted(roots.items(), key=lambda kv: -len(kv[1])): + ad = [m for m in members + if is_all_distinct(edges_f, colorings_f[m], all_named)] + label = " (contains phi_t*)" if r == phi_root else "" + print(f" class size {len(members)}: " + f"{len(ad)} all-distinct colorings{label}") + return + + +if __name__ == '__main__': + main() diff --git a/papers/dual_decomposition_minimal_counterexamples/experiments/check_conj_face_kempe.py b/papers/dual_decomposition_minimal_counterexamples/experiments/check_conj_face_kempe.py new file mode 100644 index 0000000..c894ce7 --- /dev/null +++ b/papers/dual_decomposition_minimal_counterexamples/experiments/check_conj_face_kempe.py @@ -0,0 +1,192 @@ +"""Test Conjecture 3.6: for every reduced dual of a minimal counterexample, +every proper 3-edge-coloring has a face with two same-color edges that share +a Kempe cycle with the merged edge. + +We can't run on actual counterexamples (none exist by the 4CT). Instead we +test on the structural surrogates: proper 3-edge-colorings of reduced duals +that *satisfy* chord-apex (Lemma 2.6) and the Kempe-cycle condition +(Lemma 2.7). These are the kinds of colorings a counterexample's reduced +dual would be forced to admit. + +For each such (G, face, i_red, phi), check whether some face F of H_1 and +some pair of edges (e1, e2) in partial F satisfy: + - phi(e1) = phi(e2) + - e1, e2, and merged all lie on a common {a,b}-Kempe cycle. + +If conjecture FAILS for some coloring, we have empirical evidence against. +If every coloring passes, evidence in favour. + +Run with: sage experiments/check_conj_face_kempe.py +""" +from sage.all import Graph +from sage.graphs.graph_generators import graphs + + +def dual_of(G): + G.is_planar(set_embedding=True) + faces = G.faces() + edge_to_faces = {} + for fi, face in enumerate(faces): + for u, v in face: + edge_to_faces.setdefault(frozenset((u, v)), []).append(fi) + return Graph( + [(fs[0], fs[1]) for fs in edge_to_faces.values() if len(fs) == 2], + multiedges=False, loops=False) + + +def apply_reduction(G, face, i, v_n_label): + boundary = [u for (u, v) in face] + if len(set(boundary)) != 5: return None + A = [] + for B_k in boundary: + outer = [w for w in G.neighbor_iterator(B_k) if w not in boundary] + if len(outer) != 1: return None + A.append(outer[0]) + if len(set(A)) != 5 or A[(i+3) % 5] == A[(i+4) % 5]: return None + H = G.copy() + for v in boundary: H.delete_vertex(v) + H.add_vertex(v_n_label) + side_0 = (v_n_label, A[i]) + spike = (v_n_label, A[(i+1) % 5]) + side_1 = (v_n_label, A[(i+2) % 5]) + merged = (A[(i+3) % 5], A[(i+4) % 5]) + H.add_edges([side_0, spike, side_1, merged]) + if H.has_multiple_edges() or H.has_loops(): return None + if not H.is_planar(set_embedding=True): return None + if not all(H.degree(v) == 3 for v in H.vertex_iterator()): return None + return { + 'H': H, + 'named': { + 'spike': frozenset(spike), 'side_0': frozenset(side_0), + 'side_1': frozenset(side_1), 'merged': frozenset(merged), + }, + } + + +def proper_3_edge_colorings(G): + edges = list(G.edges(labels=False)) + n = len(edges) + adj = [[] for _ in range(n)] + for i in range(n): + u, v = edges[i][0], edges[i][1] + for j in range(i): + x, y = edges[j][0], edges[j][1] + if u in (x, y) or v in (x, y): + adj[i].append(j); adj[j].append(i) + coloring = [-1] * n + results = [] + + def back(k): + if k == n: + results.append(tuple(coloring)) + return + for c in range(3): + if all(coloring[j] != c for j in adj[k]): + coloring[k] = c + back(k + 1) + coloring[k] = -1 + back(0) + return edges, results + + +def kempe_cycle(edges, coloring, start_idx, color_pair): + a, b = color_pair + if coloring[start_idx] not in (a, b): + return set() + in_sub = set(i for i in range(len(edges)) if coloring[i] in (a, b)) + visited = {start_idx} + stack = [start_idx] + while stack: + cur = stack.pop() + u, v = edges[cur][0], edges[cur][1] + for j in in_sub: + if j in visited: + continue + x, y = edges[j][0], edges[j][1] + if u in (x, y) or v in (x, y): + visited.add(j); stack.append(j) + return visited + + +def edge_idx(edges, e_frozen): + for i, e in enumerate(edges): + if frozenset((e[0], e[1])) == e_frozen: + return i + return None + + +def matches_chord_apex_kempe(edges, col, named): + idx = {role: edge_idx(edges, ns) for role, ns in named.items()} + if any(v is None for v in idx.values()): return False + c_spike = col[idx['spike']] + c_merged = col[idx['merged']] + if c_spike != c_merged: return False + c_s0 = col[idx['side_0']]; c_s1 = col[idx['side_1']] + kc0 = kempe_cycle(edges, col, idx['spike'], (c_spike, c_s0)) + if idx['side_0'] not in kc0 or idx['merged'] not in kc0: return False + kc1 = kempe_cycle(edges, col, idx['spike'], (c_spike, c_s1)) + if idx['side_1'] not in kc1 or idx['merged'] not in kc1: return False + return True + + +def conjecture_holds_for(H, edges, col, named): + """Returns (F, e1, e2, kc) if some face F has two same-color edges (e1, e2) + and both, together with merged, lie on a Kempe cycle kc. Else None.""" + merged_idx = edge_idx(edges, named['merged']) + c_merged = col[merged_idx] + # All Kempe cycles through merged (one per color pair (c_merged, c')) + kempe_cycles = [] + for c_prime in range(3): + if c_prime == c_merged: continue + kc = kempe_cycle(edges, col, merged_idx, (c_merged, c_prime)) + kempe_cycles.append(kc) + for face in H.faces(): + face_edge_indices = [] + for u, v in face: + ei = edge_idx(edges, frozenset((u, v))) + if ei is not None: + face_edge_indices.append(ei) + for i in range(len(face_edge_indices)): + for j in range(i + 1, len(face_edge_indices)): + e1, e2 = face_edge_indices[i], face_edge_indices[j] + if col[e1] != col[e2]: continue + for kc in kempe_cycles: + if e1 in kc and e2 in kc: + return face, e1, e2, kc + return None + + +def main(): + for n in [12, 14, 15]: + print(f"=== n = {n} ===") + try: + triangulations = list(graphs.triangulations(n, minimum_degree=5)) + except Exception as ex: + print(f" cannot enumerate: {ex}"); continue + for tri_idx, G in enumerate(triangulations, start=1): + G.is_planar(set_embedding=True) + D = dual_of(G); D.is_planar(set_embedding=True) + for face_no, face in enumerate( + f for f in D.faces() if len(f) == 5): + for i_red in range(5): + res = apply_reduction(D, face, i_red, 9999) + if res is None: continue + H = res['H']; named = res['named'] + H.is_planar(set_embedding=True) + edges, colorings = proper_3_edge_colorings(H) + cand = [c for c in colorings + if matches_chord_apex_kempe(edges, c, named)] + if not cand: continue + n_pass = sum(1 for c in cand + if conjecture_holds_for(H, edges, c, named) + is not None) + n_fail = len(cand) - n_pass + status = "PASSED" if n_fail == 0 else "*** FAILED ***" + print(f" n={n} tri#{tri_idx} face#{face_no} i_red={i_red}: " + f"{len(cand)} chord-apex+Kempe colorings; " + f"{n_pass} satisfy conjecture, {n_fail} fail. " + f"{status}") + + +if __name__ == '__main__': + main() diff --git a/papers/dual_decomposition_minimal_counterexamples/experiments/check_conj_face_kempe_n15.py b/papers/dual_decomposition_minimal_counterexamples/experiments/check_conj_face_kempe_n15.py new file mode 100644 index 0000000..defa88d --- /dev/null +++ b/papers/dual_decomposition_minimal_counterexamples/experiments/check_conj_face_kempe_n15.py @@ -0,0 +1,59 @@ +"""Run conjecture 3.6 test specifically on n=15 with progress output.""" +from sage.all import Graph +from sage.graphs.graph_generators import graphs +import sys + +# Reuse helpers from check_conj_face_kempe.py by importing +sys.path.insert(0, '/Users/didericis/Code/math-research/papers/dual_decomposition_minimal_counterexamples/experiments') +from check_conj_face_kempe import ( + dual_of, apply_reduction, proper_3_edge_colorings, + kempe_cycle, edge_idx, matches_chord_apex_kempe, + conjecture_holds_for +) + + +def main(): + n = 15 + print(f"=== n = {n} ===") + triangulations = list(graphs.triangulations(n, minimum_degree=5)) + print(f" Found {len(triangulations)} triangulations.") + total_cand = 0 + total_pass = 0 + total_fail = 0 + for tri_idx, G in enumerate(triangulations, start=1): + G.is_planar(set_embedding=True) + D = dual_of(G); D.is_planar(set_embedding=True) + pentagonal_faces = [f for f in D.faces() if len(f) == 5] + for face_no, face in enumerate(pentagonal_faces): + for i_red in range(5): + res = apply_reduction(D, face, i_red, 9999) + if res is None: continue + H = res['H']; named = res['named'] + H.is_planar(set_embedding=True) + edges, colorings = proper_3_edge_colorings(H) + cand = [c for c in colorings + if matches_chord_apex_kempe(edges, c, named)] + if not cand: continue + n_pass = sum(1 for c in cand + if conjecture_holds_for(H, edges, c, named) + is not None) + n_fail = len(cand) - n_pass + total_cand += len(cand) + total_pass += n_pass + total_fail += n_fail + status = "PASSED" if n_fail == 0 else "*** FAILED ***" + print(f" tri#{tri_idx} face#{face_no} i_red={i_red}: " + f"{len(cand)} chord-apex+Kempe; {n_pass} pass, " + f"{n_fail} fail. {status}") + sys.stdout.flush() + if tri_idx % 5 == 0: + print(f" ... finished tri#{tri_idx}/{len(triangulations)}; " + f"cumulative cand={total_cand}, pass={total_pass}, " + f"fail={total_fail}") + sys.stdout.flush() + print(f"\nTotal: {total_cand} chord-apex+Kempe colorings tested; " + f"{total_pass} pass, {total_fail} fail.") + + +if __name__ == '__main__': + main() diff --git a/papers/dual_decomposition_minimal_counterexamples/experiments/check_constrained_feasibility.py b/papers/dual_decomposition_minimal_counterexamples/experiments/check_constrained_feasibility.py new file mode 100644 index 0000000..1d2909b --- /dev/null +++ b/papers/dual_decomposition_minimal_counterexamples/experiments/check_constrained_feasibility.py @@ -0,0 +1,259 @@ +"""Constrained 3-edge-colouring feasibility on H_t*. + +The chord-apex (Lemma 2.6) and Kempe-cycle (Lemma 2.7) lemmas give proven +constraints on proper 3-edge-colourings of H_1 when G is a minimal +counterexample. The step-1 constraints, *interpreted on H_t*, are: + + (C1) phi(spike_1) = phi(merged_1) [chord-apex] + (K0) the {phi(spike_1), phi(side_0_1)}-Kempe cycle of H_t* through + spike_1 contains side_0_1 and merged_1 + (K1) the {phi(spike_1), phi(side_1_1)}-Kempe cycle of H_t* through + spike_1 contains side_1_1 and merged_1 + +If G is a minimal counterexample then every proper 3-edge-colouring of H_t* +that *lifts back* to a proper 3-edge-colouring of H_1 must satisfy (C1) + +(K0) + (K1) on H_1; the Kempe-cycle structure on H_t* and H_1 can differ, +but we test the H_t*-interpreted versions here as the natural constraint +set the algorithm propagates. + +For each min-deg-5 triangulation G and each (face, i_red) we enumerate +proper 3-edge-colourings of H_t* and count those satisfying these step-1 +constraints. If the constrained problem is INFEASIBLE on H_t* for some G +in our test set, that would be a hint that constraints alone can rule out +3-edge-colourability of H_t* -- a potential mechanism for proving smaller +counterexamples exist. + +Run with: sage experiments/check_constrained_feasibility.py +""" +from sage.all import Graph +from sage.graphs.graph_generators import graphs +from sage.graphs.graph_coloring import edge_coloring +import sys + + +def dual_of(G): + G.is_planar(set_embedding=True) + faces = G.faces() + edge_to_faces = {} + for fi, face in enumerate(faces): + for u, v in face: + edge_to_faces.setdefault(frozenset((u, v)), []).append(fi) + return Graph( + [(fs[0], fs[1]) for fs in edge_to_faces.values() if len(fs) == 2], + multiedges=False, loops=False) + + +def proper_3_edge_colorings(G): + edges = list(G.edges(labels=False)) + n = len(edges) + adj = [[] for _ in range(n)] + for i in range(n): + u, v = edges[i][0], edges[i][1] + for j in range(i): + x, y = edges[j][0], edges[j][1] + if u in (x, y) or v in (x, y): + adj[i].append(j); adj[j].append(i) + coloring = [-1] * n + results = [] + + def back(k): + if k == n: + results.append(tuple(coloring)) + return + for c in range(3): + if all(coloring[j] != c for j in adj[k]): + coloring[k] = c + back(k + 1) + coloring[k] = -1 + back(0) + return edges, results + + +def kempe_cycle(edges, coloring, start_idx, color_pair): + a, b = color_pair + if coloring[start_idx] not in (a, b): + return set() + in_sub = set(i for i in range(len(edges)) if coloring[i] in (a, b)) + visited = {start_idx} + stack = [start_idx] + while stack: + cur = stack.pop() + u, v = edges[cur][0], edges[cur][1] + for j in in_sub: + if j in visited: + continue + x, y = edges[j][0], edges[j][1] + if u in (x, y) or v in (x, y): + visited.add(j); stack.append(j) + return visited + + +def edge_idx(edges, e_frozen): + for i, e in enumerate(edges): + if frozenset((e[0], e[1])) == e_frozen: + return i + return None + + +def apply_reduction(G, face, i, v_n_label): + boundary = [u for (u, v) in face] + if len(set(boundary)) != 5: return None + A = [] + for B_k in boundary: + outer = [w for w in G.neighbor_iterator(B_k) if w not in boundary] + if len(outer) != 1: return None + A.append(outer[0]) + if len(set(A)) != 5 or A[(i+3) % 5] == A[(i+4) % 5]: return None + H = G.copy() + for v in boundary: H.delete_vertex(v) + H.add_vertex(v_n_label) + side_0 = (v_n_label, A[i]) + spike = (v_n_label, A[(i+1) % 5]) + side_1 = (v_n_label, A[(i+2) % 5]) + merged = (A[(i+3) % 5], A[(i+4) % 5]) + H.add_edges([side_0, spike, side_1, merged]) + if H.has_multiple_edges() or H.has_loops(): return None + if not H.is_planar(set_embedding=True): return None + if not all(H.degree(v) == 3 for v in H.vertex_iterator()): return None + return { + 'H': H, + 'named': { + 'spike': frozenset(spike), 'side_0': frozenset(side_0), + 'side_1': frozenset(side_1), 'merged': frozenset(merged), + }, + } + + +def find_safe_pentagonal_face(G, protected): + for face in G.faces(): + if len(face) != 5: continue + boundary = [u for (u, v) in face] + boundary_edges = [frozenset([u, v]) for (u, v) in face] + externals, A, ok = [], [], True + for B_k in boundary: + outer = [w for w in G.neighbor_iterator(B_k) if w not in boundary] + if len(outer) != 1: ok = False; break + externals.append(frozenset([B_k, outer[0]])); A.append(outer[0]) + if not ok: continue + if any(e in protected for e in boundary_edges + externals): continue + return boundary, externals, A + return None + + +def valid_index(f_vec, A): + for i in range(5): + if f_vec[(i+3) % 5] != f_vec[(i+4) % 5]: continue + if len({f_vec[i], f_vec[(i+1) % 5], f_vec[(i+2) % 5]}) != 3: continue + if A[(i+3) % 5] == A[(i+4) % 5]: continue + return i + return None + + +def run_to_completion(H, phi_dict, named_step1, vn_start=10000): + H = H.copy() + coloring = dict(phi_dict) + all_named = [named_step1] + E = set(named_step1.values()) + next_vn = vn_start + while True: + H.is_planar(set_embedding=True) + result = find_safe_pentagonal_face(H, E) + if result is None: break + boundary, externals, A = result + f_vec = [coloring[e] for e in externals] + i_t = valid_index(f_vec, A) + if i_t is None: break + v_n = next_vn; next_vn += 1 + H_new = H.copy() + for v in boundary: H_new.delete_vertex(v) + H_new.add_vertex(v_n) + s0 = (v_n, A[i_t]); sp = (v_n, A[(i_t+1) % 5]) + s1 = (v_n, A[(i_t+2) % 5]); mg = (A[(i_t+3) % 5], A[(i_t+4) % 5]) + H_new.add_edges([s0, sp, s1, mg]) + if H_new.has_multiple_edges() or H_new.has_loops(): break + if not H_new.is_planar(set_embedding=True): break + H = H_new + coloring = {e: c for e, c in coloring.items() + if not any(u in boundary for u in e)} + coloring[frozenset(s0)] = f_vec[i_t] + coloring[frozenset(sp)] = f_vec[(i_t+1) % 5] + coloring[frozenset(s1)] = f_vec[(i_t+2) % 5] + coloring[frozenset(mg)] = f_vec[(i_t+3) % 5] + all_named.append({ + 'spike': frozenset(sp), 'side_0': frozenset(s0), + 'side_1': frozenset(s1), 'merged': frozenset(mg), + }) + E |= set(all_named[-1].values()) + return H, coloring, all_named + + +def check_constraints(edges, col, named): + """Check (C1) + (K0) + (K1) on this colouring.""" + idx = {role: edge_idx(edges, ns) for role, ns in named.items()} + if any(v is None for v in idx.values()): + return False, False, False + c_spike = col[idx['spike']] + c_merged = col[idx['merged']] + C1 = (c_spike == c_merged) + if not C1: + return False, False, False + c_s0 = col[idx['side_0']]; c_s1 = col[idx['side_1']] + kc0 = kempe_cycle(edges, col, idx['spike'], (c_spike, c_s0)) + kc1 = kempe_cycle(edges, col, idx['spike'], (c_spike, c_s1)) + K0 = idx['side_0'] in kc0 and idx['merged'] in kc0 + K1 = idx['side_1'] in kc1 and idx['merged'] in kc1 + return C1, K0, K1 + + +def run_case(G, n, tri_idx): + G.is_planar(set_embedding=True) + D = dual_of(G); D.is_planar(set_embedding=True) + for face_n, face in enumerate([f for f in D.faces() if len(f) == 5]): + for i_red in range(5): + res = apply_reduction(D, face, i_red, 9999) + if res is None: continue + H_1, named_1 = res['H'], res['named'] + # Default phi_1: Sage's edge_coloring + try: + classes = edge_coloring(H_1, value_only=False) + except Exception: + continue + if len(classes) > 3: continue + phi_1_dict = {} + for k, edge_list in enumerate(classes): + for u, v in edge_list: + phi_1_dict[frozenset([u, v])] = k + H_final, _, all_named = run_to_completion(H_1, phi_1_dict, named_1) + edges_f, colorings_f = proper_3_edge_colorings(H_final) + n_total = len(colorings_f) + n_c1 = 0; n_c1_k0 = 0; n_c1_k1 = 0; n_all = 0 + for col in colorings_f: + C1, K0, K1 = check_constraints(edges_f, col, named_1) + if C1: n_c1 += 1 + if C1 and K0: n_c1_k0 += 1 + if C1 and K1: n_c1_k1 += 1 + if C1 and K0 and K1: n_all += 1 + feasible = n_all > 0 + print(f" n={n} tri#{tri_idx} face#{face_n} i_red={i_red}: " + f"|V(H_t*)|={H_final.order()}, |E|={H_final.size()}, " + f"colorings={n_total}, " + f"C1={n_c1}, C1+K0={n_c1_k0}, C1+K1={n_c1_k1}, " + f"C1+K0+K1={n_all} " + f"{'OK' if feasible else '*** INFEASIBLE ***'}") + sys.stdout.flush() + return # one (face, i_red) per triangulation + + +def main(max_n=15): + for n in range(12, max_n + 1): + print(f"\n=== n = {n} ===") + try: + triangulations = list(graphs.triangulations(n, minimum_degree=5)) + except Exception as ex: + print(f" cannot enumerate: {ex}"); continue + for tri_idx, G in enumerate(triangulations, start=1): + run_case(G, n, tri_idx) + + +if __name__ == '__main__': + main() diff --git a/papers/dual_decomposition_minimal_counterexamples/experiments/check_kempe_class.py b/papers/dual_decomposition_minimal_counterexamples/experiments/check_kempe_class.py new file mode 100644 index 0000000..3d03299 --- /dev/null +++ b/papers/dual_decomposition_minimal_counterexamples/experiments/check_kempe_class.py @@ -0,0 +1,183 @@ +"""Check empirically whether all proper 3-edge-colorings of a cubic plane +graph form a single Kempe equivalence class. + +For each test graph: + 1. enumerate all proper 3-edge-colorings; + 2. build a multigraph K whose vertices are the colorings and whose edges + connect pairs related by a single Kempe swap (swapping two colors on + one cycle of the 2-color subgraph); + 3. report the number of connected components of K (= number of Kempe + classes). + +Test inputs: + - Dodecahedron's reduced dual (16 v, 24 e), built as in + check_dodecahedron_kempe.py; + - The n=14 reduced dual found by search_kempe_property.py (20 v, 30 e). +""" +from sage.all import Graph +from sage.graphs.graph_generators import graphs +import sys + + +def all_proper_3_edge_colorings(G): + edges = list(G.edges(labels=False)) + n = len(edges) + adj = [[] for _ in range(n)] + for i in range(n): + u, v = edges[i][0], edges[i][1] + for j in range(i): + x, y = edges[j][0], edges[j][1] + if u in (x, y) or v in (x, y): + adj[i].append(j) + adj[j].append(i) + coloring = [-1] * n + results = [] + + def back(k): + if k == n: + results.append(tuple(coloring)) + return + for c in range(3): + if all(coloring[j] != c for j in adj[k]): + coloring[k] = c + back(k + 1) + coloring[k] = -1 + back(0) + return edges, results + + +def kempe_cycles_of(edges, coloring, color_pair): + """List of connected components (as sorted tuples of edge indices) in + the subgraph of edges with color in color_pair.""" + a, b = color_pair + in_sub = [i for i in range(len(edges)) if coloring[i] in (a, b)] + in_set = set(in_sub) + visited = set() + components = [] + for start in in_sub: + if start in visited: + continue + comp = [] + stack = [start] + visited.add(start) + while stack: + cur = stack.pop() + comp.append(cur) + u, v = edges[cur][0], edges[cur][1] + for j in in_set: + if j in visited: + continue + x, y = edges[j][0], edges[j][1] + if u in (x, y) or v in (x, y): + visited.add(j) + stack.append(j) + components.append(tuple(sorted(comp))) + return components + + +def swap_on_cycle(coloring, cycle_edges, color_pair): + a, b = color_pair + swap = list(coloring) + for i in cycle_edges: + if swap[i] == a: + swap[i] = b + elif swap[i] == b: + swap[i] = a + return tuple(swap) + + +def kempe_components(G): + edges, colorings = all_proper_3_edge_colorings(G) + print(f" {len(colorings)} proper 3-edge-colorings") + idx = {c: i for i, c in enumerate(colorings)} + parent = list(range(len(colorings))) + + def find(x): + while parent[x] != x: + parent[x] = parent[parent[x]] + x = parent[x] + return x + + def union(x, y): + rx, ry = find(x), find(y) + if rx != ry: + parent[rx] = ry + + for col in colorings: + for a, b in [(0, 1), (0, 2), (1, 2)]: + for cyc in kempe_cycles_of(edges, col, (a, b)): + new_col = swap_on_cycle(col, cyc, (a, b)) + if new_col == col: + continue + if new_col in idx: + union(idx[col], idx[new_col]) + n_classes = len({find(i) for i in range(len(colorings))}) + print(f" Kempe equivalence classes: {n_classes}") + return n_classes + + +def dodecahedron_reduced_dual(): + edges = [] + for k in range(5): + edges.append((('b', k), ('c', k))) + edges.append((('b', k), ('c', (k - 1) % 5))) + edges.append((('c', k), ('d', k))) + edges.append((('d', k), ('d', (k + 1) % 5))) + edges.append(('v_n', ('b', 0))) + edges.append(('v_n', ('b', 1))) + edges.append(('v_n', ('b', 2))) + edges.append((('b', 3), ('b', 4))) + return Graph(edges, multiedges=False, loops=False) + + +def n14_reduced_dual(): + # First min-degree-5 plantri triangulation on 14 vertices, reduced at the + # first pentagonal face with i_red = 1 (matches search_kempe_property.py). + G = next(graphs.triangulations(14, minimum_degree=5)) + G.is_planar(set_embedding=True) + faces = G.faces() + edge_to_faces = {} + for fi, face in enumerate(faces): + for u, v in face: + edge_to_faces.setdefault(frozenset((u, v)), []).append(fi) + dual_edges = [(fs[0], fs[1]) for fs in edge_to_faces.values() if len(fs) == 2] + D = Graph(dual_edges, multiedges=False, loops=False) + D.is_planar(set_embedding=True) + # use first pentagonal face, i_red = 1 + face = next(f for f in D.faces() if len(f) == 5) + boundary = [u for (u, v) in face] + A = [] + for B_k in boundary: + outer = [w for w in D.neighbor_iterator(B_k) if w not in boundary] + A.append(outer[0]) + H = D.copy() + for v in boundary: + H.delete_vertex(v) + vn = '__v_n__' + H.add_vertex(vn) + H.add_edge(vn, A[1]) # spike + H.add_edge(vn, A[0]) # side_0 + H.add_edge(vn, A[2]) # side_1 + H.add_edge(A[3], A[4]) # merged + H.is_planar(set_embedding=True) + return H + + +def main(): + print("Dodecahedron's reduced dual:") + G1 = dodecahedron_reduced_dual() + kempe_components(G1) + + print() + print("n=14 reduced dual (first plantri triangulation, i_red=1):") + G2 = n14_reduced_dual() + kempe_components(G2) + + print() + print("Small sanity check: K_4") + K4 = graphs.CompleteGraph(4) + kempe_components(K4) + + +if __name__ == '__main__': + main() diff --git a/papers/dual_decomposition_minimal_counterexamples/experiments/check_kempe_class_invariance.py b/papers/dual_decomposition_minimal_counterexamples/experiments/check_kempe_class_invariance.py new file mode 100644 index 0000000..9d2cb4d --- /dev/null +++ b/papers/dual_decomposition_minimal_counterexamples/experiments/check_kempe_class_invariance.py @@ -0,0 +1,288 @@ +"""Investigate the conjecture: H_t* has the same number of Kempe equivalence +classes as H_1. + +For each min-deg-5 triangulation G (up to some n) and each reduction index +i_red in {0,...,4}: + - Build H_1 from the first pentagonal face of G' = dual(G). + - Count Kempe classes of H_1. + - Run Algorithm 3.1 to completion with Sage's edge_coloring as phi_1. + - Count Kempe classes of H_t*. + - Print a row. + +Run with: sage experiments/check_kempe_class_invariance.py +""" +from sage.all import Graph +from sage.graphs.graph_generators import graphs +from sage.graphs.graph_coloring import edge_coloring +import sys + + +def dual_of(G): + G.is_planar(set_embedding=True) + faces = G.faces() + edge_to_faces = {} + for fi, face in enumerate(faces): + for u, v in face: + edge_to_faces.setdefault(frozenset((u, v)), []).append(fi) + dual_edges = [(fs[0], fs[1]) for fs in edge_to_faces.values() if len(fs) == 2] + return Graph(dual_edges, multiedges=False, loops=False) + + +def proper_3_edge_colorings(G): + edges = list(G.edges(labels=False)) + n = len(edges) + adj = [[] for _ in range(n)] + for i in range(n): + u, v = edges[i][0], edges[i][1] + for j in range(i): + x, y = edges[j][0], edges[j][1] + if u in (x, y) or v in (x, y): + adj[i].append(j) + adj[j].append(i) + coloring = [-1] * n + results = [] + + def back(k): + if k == n: + results.append(tuple(coloring)) + return + for c in range(3): + if all(coloring[j] != c for j in adj[k]): + coloring[k] = c + back(k + 1) + coloring[k] = -1 + + back(0) + return edges, results + + +def kempe_cycle(edges, coloring, start_idx, color_pair): + a, b = color_pair + if coloring[start_idx] not in (a, b): + return set() + in_sub = set(i for i in range(len(edges)) if coloring[i] in (a, b)) + visited = {start_idx} + stack = [start_idx] + while stack: + cur = stack.pop() + u, v = edges[cur][0], edges[cur][1] + for j in in_sub: + if j in visited: + continue + x, y = edges[j][0], edges[j][1] + if u in (x, y) or v in (x, y): + visited.add(j) + stack.append(j) + return visited + + +def num_kempe_classes(G): + """Count the Kempe equivalence classes of proper 3-edge-colorings of G.""" + edges, colorings = proper_3_edge_colorings(G) + if not colorings: + return None, 0 + n = len(colorings) + parent = list(range(n)) + + def find(x): + while parent[x] != x: + parent[x] = parent[parent[x]] + x = parent[x] + return x + + def union(x, y): + rx, ry = find(x), find(y) + if rx != ry: + parent[rx] = ry + + col_idx = {c: i for i, c in enumerate(colorings)} + for c_idx, col in enumerate(colorings): + for pair in [(0, 1), (0, 2), (1, 2)]: + visited = set() + for start in range(len(edges)): + if col[start] not in pair or start in visited: + continue + cyc = kempe_cycle(edges, col, start, pair) + visited |= cyc + a, b = pair + new_col = list(col) + for k in cyc: + if new_col[k] == a: + new_col[k] = b + elif new_col[k] == b: + new_col[k] = a + new_col = tuple(new_col) + if new_col != col and new_col in col_idx: + union(c_idx, col_idx[new_col]) + classes = len({find(i) for i in range(n)}) + return n, classes + + +def apply_reduction(G, face, i, v_n_label): + boundary = [u for (u, v) in face] + if len(set(boundary)) != 5: + return None + A = [] + for B_k in boundary: + outer = [w for w in G.neighbor_iterator(B_k) if w not in boundary] + if len(outer) != 1: + return None + A.append(outer[0]) + if len(set(A)) != 5: + return None + if A[(i + 3) % 5] == A[(i + 4) % 5]: + return None + H = G.copy() + for v in boundary: + H.delete_vertex(v) + H.add_vertex(v_n_label) + side_0 = (v_n_label, A[i]) + spike = (v_n_label, A[(i + 1) % 5]) + side_1 = (v_n_label, A[(i + 2) % 5]) + merged = (A[(i + 3) % 5], A[(i + 4) % 5]) + H.add_edges([side_0, spike, side_1, merged]) + if H.has_multiple_edges() or H.has_loops(): + return None + if not H.is_planar(set_embedding=True): + return None + if not all(H.degree(v) == 3 for v in H.vertex_iterator()): + return None + return { + 'H': H, 'A': A, + 'named': { + 'spike': frozenset(spike), + 'side_0': frozenset(side_0), + 'side_1': frozenset(side_1), + 'merged': frozenset(merged), + }, + } + + +def find_safe_pentagonal_face(G, protected): + for face in G.faces(): + if len(face) != 5: + continue + boundary = [u for (u, v) in face] + boundary_edges = [frozenset([u, v]) for (u, v) in face] + externals = [] + A = [] + ok = True + for B_k in boundary: + outer = [w for w in G.neighbor_iterator(B_k) if w not in boundary] + if len(outer) != 1: + ok = False + break + externals.append(frozenset([B_k, outer[0]])) + A.append(outer[0]) + if not ok: + continue + if any(e in protected for e in boundary_edges + externals): + continue + return boundary, externals, A + return None + + +def valid_index(f_vec, A): + for i in range(5): + if f_vec[(i + 3) % 5] != f_vec[(i + 4) % 5]: + continue + if len({f_vec[i], f_vec[(i + 1) % 5], f_vec[(i + 2) % 5]}) != 3: + continue + if A[(i + 3) % 5] == A[(i + 4) % 5]: + continue + return i + return None + + +def run_algorithm_to_completion(H, phi_1_coloring_dict, named_step1, + vn_start=10000): + H = H.copy() + coloring = dict(phi_1_coloring_dict) + E = set(named_step1.values()) + next_vn = vn_start + while True: + H.is_planar(set_embedding=True) + result = find_safe_pentagonal_face(H, E) + if result is None: + break + boundary, externals, A = result + f_vec = [coloring[e] for e in externals] + i_t = valid_index(f_vec, A) + if i_t is None: + break + v_n = next_vn + next_vn += 1 + H_new = H.copy() + for v in boundary: + H_new.delete_vertex(v) + H_new.add_vertex(v_n) + side_0 = (v_n, A[i_t]) + spike = (v_n, A[(i_t + 1) % 5]) + side_1 = (v_n, A[(i_t + 2) % 5]) + merged = (A[(i_t + 3) % 5], A[(i_t + 4) % 5]) + H_new.add_edges([side_0, spike, side_1, merged]) + if H_new.has_multiple_edges() or H_new.has_loops(): + break + if not H_new.is_planar(set_embedding=True): + break + H = H_new + coloring = {e: c for e, c in coloring.items() + if not any(u in boundary for u in e)} + coloring[frozenset(side_0)] = f_vec[i_t] + coloring[frozenset(spike)] = f_vec[(i_t + 1) % 5] + coloring[frozenset(side_1)] = f_vec[(i_t + 2) % 5] + coloring[frozenset(merged)] = f_vec[(i_t + 3) % 5] + E |= {frozenset(spike), frozenset(side_0), frozenset(side_1), + frozenset(merged)} + return H, coloring + + +def main(): + print(f"{'n':>3} {'tri#':>5} {'i_red':>5} | " + f"{'|V(H_1)|':>9} {'|E(H_1)|':>9} {'#col(H_1)':>10} {'#K(H_1)':>8} | " + f"{'|V(H_t*)|':>10} {'|E(H_t*)|':>10} {'#col(H_t*)':>11} {'#K(H_t*)':>10}") + print("-" * 120) + for n in [12, 14]: + try: + triangulations = list(graphs.triangulations(n, minimum_degree=5)) + except Exception as ex: + print(f" cannot enumerate n={n}: {ex}") + continue + for tri_idx, G in enumerate(triangulations, start=1): + G_copy = G.copy() + G_copy.is_planar(set_embedding=True) + D = dual_of(G_copy) + D.is_planar(set_embedding=True) + # iterate over all pentagonal faces (or just the first) + faces = [f for f in D.faces() if len(f) == 5] + if not faces: + continue + face = faces[0] + for i_red in range(5): + res = apply_reduction(D, face, i_red, 9999) + if res is None: + continue + H_1 = res['H'] + # count Kempe classes of H_1 + n_col_h1, n_kc_h1 = num_kempe_classes(H_1) + # run algorithm to completion with Sage's edge_coloring as phi_1 + classes = edge_coloring(H_1, value_only=False) + if len(classes) > 3: + continue + phi_1_dict = {} + for k, edge_list in enumerate(classes): + for u, v in edge_list: + phi_1_dict[frozenset([u, v])] = k + H_final, _ = run_algorithm_to_completion(H_1, phi_1_dict, + res['named']) + n_col_hf, n_kc_hf = num_kempe_classes(H_final) + same = "same" if n_kc_h1 == n_kc_hf else "DIFFERENT" + print(f"{n:>3} {tri_idx:>5} {i_red:>5} | " + f"{H_1.order():>9} {H_1.size():>9} {n_col_h1:>10} {n_kc_h1:>8} | " + f"{H_final.order():>10} {H_final.size():>10} " + f"{n_col_hf:>11} {n_kc_hf:>10} {same}") + sys.stdout.flush() + + +if __name__ == '__main__': + main() diff --git a/papers/dual_decomposition_minimal_counterexamples/experiments/check_kempe_class_monotone.py b/papers/dual_decomposition_minimal_counterexamples/experiments/check_kempe_class_monotone.py new file mode 100644 index 0000000..3ad7436 --- /dev/null +++ b/papers/dual_decomposition_minimal_counterexamples/experiments/check_kempe_class_monotone.py @@ -0,0 +1,310 @@ +"""Investigate the conjecture: + #(Kempe classes of H_t*) <= #(Kempe classes of H_1). + +For each min-deg-5 triangulation G and each (face, i_red) choice giving a +valid H_1, vary phi_1 across many proper 3-edge-colorings of H_1 -- so we +exercise multiple algorithm executions, each potentially producing a +different H_t*. For each execution, count Kempe classes of H_t* and compare +to H_1. + +Reports any case where #classes(H_t*) > #classes(H_1) (counterexample to +the conjecture). + +Run with: sage experiments/check_kempe_class_monotone.py +""" +from sage.all import Graph +from sage.graphs.graph_generators import graphs +import sys +import time + + +def dual_of(G): + G.is_planar(set_embedding=True) + faces = G.faces() + edge_to_faces = {} + for fi, face in enumerate(faces): + for u, v in face: + edge_to_faces.setdefault(frozenset((u, v)), []).append(fi) + dual_edges = [(fs[0], fs[1]) for fs in edge_to_faces.values() if len(fs) == 2] + return Graph(dual_edges, multiedges=False, loops=False) + + +def proper_3_edge_colorings(G): + edges = list(G.edges(labels=False)) + n = len(edges) + adj = [[] for _ in range(n)] + for i in range(n): + u, v = edges[i][0], edges[i][1] + for j in range(i): + x, y = edges[j][0], edges[j][1] + if u in (x, y) or v in (x, y): + adj[i].append(j) + adj[j].append(i) + coloring = [-1] * n + results = [] + + def back(k): + if k == n: + results.append(tuple(coloring)) + return + for c in range(3): + if all(coloring[j] != c for j in adj[k]): + coloring[k] = c + back(k + 1) + coloring[k] = -1 + + back(0) + return edges, results + + +def kempe_cycle(edges, coloring, start_idx, color_pair): + a, b = color_pair + if coloring[start_idx] not in (a, b): + return set() + in_sub = set(i for i in range(len(edges)) if coloring[i] in (a, b)) + visited = {start_idx} + stack = [start_idx] + while stack: + cur = stack.pop() + u, v = edges[cur][0], edges[cur][1] + for j in in_sub: + if j in visited: + continue + x, y = edges[j][0], edges[j][1] + if u in (x, y) or v in (x, y): + visited.add(j) + stack.append(j) + return visited + + +def num_kempe_classes(G): + edges, colorings = proper_3_edge_colorings(G) + if not colorings: + return 0, 0 + n = len(colorings) + parent = list(range(n)) + + def find(x): + while parent[x] != x: + parent[x] = parent[parent[x]] + x = parent[x] + return x + + def union(x, y): + rx, ry = find(x), find(y) + if rx != ry: + parent[rx] = ry + + col_idx = {c: i for i, c in enumerate(colorings)} + for c_idx, col in enumerate(colorings): + for pair in [(0, 1), (0, 2), (1, 2)]: + visited = set() + for start in range(len(edges)): + if col[start] not in pair or start in visited: + continue + cyc = kempe_cycle(edges, col, start, pair) + visited |= cyc + a, b = pair + new_col = list(col) + for k in cyc: + if new_col[k] == a: + new_col[k] = b + elif new_col[k] == b: + new_col[k] = a + new_col = tuple(new_col) + if new_col != col and new_col in col_idx: + union(c_idx, col_idx[new_col]) + classes = len({find(i) for i in range(n)}) + return n, classes + + +def apply_reduction(G, face, i, v_n_label): + boundary = [u for (u, v) in face] + if len(set(boundary)) != 5: + return None + A = [] + for B_k in boundary: + outer = [w for w in G.neighbor_iterator(B_k) if w not in boundary] + if len(outer) != 1: + return None + A.append(outer[0]) + if len(set(A)) != 5: + return None + if A[(i + 3) % 5] == A[(i + 4) % 5]: + return None + H = G.copy() + for v in boundary: + H.delete_vertex(v) + H.add_vertex(v_n_label) + side_0 = (v_n_label, A[i]) + spike = (v_n_label, A[(i + 1) % 5]) + side_1 = (v_n_label, A[(i + 2) % 5]) + merged = (A[(i + 3) % 5], A[(i + 4) % 5]) + H.add_edges([side_0, spike, side_1, merged]) + if H.has_multiple_edges() or H.has_loops(): + return None + if not H.is_planar(set_embedding=True): + return None + if not all(H.degree(v) == 3 for v in H.vertex_iterator()): + return None + return { + 'H': H, 'A': A, + 'named': { + 'spike': frozenset(spike), + 'side_0': frozenset(side_0), + 'side_1': frozenset(side_1), + 'merged': frozenset(merged), + }, + } + + +def find_safe_pentagonal_face(G, protected): + for face in G.faces(): + if len(face) != 5: + continue + boundary = [u for (u, v) in face] + boundary_edges = [frozenset([u, v]) for (u, v) in face] + externals = [] + A = [] + ok = True + for B_k in boundary: + outer = [w for w in G.neighbor_iterator(B_k) if w not in boundary] + if len(outer) != 1: + ok = False + break + externals.append(frozenset([B_k, outer[0]])) + A.append(outer[0]) + if not ok: + continue + if any(e in protected for e in boundary_edges + externals): + continue + return boundary, externals, A + return None + + +def valid_index(f_vec, A): + for i in range(5): + if f_vec[(i + 3) % 5] != f_vec[(i + 4) % 5]: + continue + if len({f_vec[i], f_vec[(i + 1) % 5], f_vec[(i + 2) % 5]}) != 3: + continue + if A[(i + 3) % 5] == A[(i + 4) % 5]: + continue + return i + return None + + +def run_algorithm_to_completion(H, phi_1_dict, named_step1, vn_start=10000): + H = H.copy() + coloring = dict(phi_1_dict) + E = set(named_step1.values()) + next_vn = vn_start + while True: + H.is_planar(set_embedding=True) + result = find_safe_pentagonal_face(H, E) + if result is None: + break + boundary, externals, A = result + f_vec = [coloring[e] for e in externals] + i_t = valid_index(f_vec, A) + if i_t is None: + break + v_n = next_vn + next_vn += 1 + H_new = H.copy() + for v in boundary: + H_new.delete_vertex(v) + H_new.add_vertex(v_n) + side_0 = (v_n, A[i_t]) + spike = (v_n, A[(i_t + 1) % 5]) + side_1 = (v_n, A[(i_t + 2) % 5]) + merged = (A[(i_t + 3) % 5], A[(i_t + 4) % 5]) + H_new.add_edges([side_0, spike, side_1, merged]) + if H_new.has_multiple_edges() or H_new.has_loops(): + break + if not H_new.is_planar(set_embedding=True): + break + H = H_new + coloring = {e: c for e, c in coloring.items() + if not any(u in boundary for u in e)} + coloring[frozenset(side_0)] = f_vec[i_t] + coloring[frozenset(spike)] = f_vec[(i_t + 1) % 5] + coloring[frozenset(side_1)] = f_vec[(i_t + 2) % 5] + coloring[frozenset(merged)] = f_vec[(i_t + 3) % 5] + E |= {frozenset(spike), frozenset(side_0), frozenset(side_1), + frozenset(merged)} + return H + + +def main(max_n=15, time_budget_sec=600): + start = time.time() + violations = [] + for n in range(12, max_n + 1): + if time.time() - start > time_budget_sec: + print(f"Time budget exhausted at n={n}.") + break + print(f"\n=== n = {n} ===") + try: + triangulations = list(graphs.triangulations(n, minimum_degree=5)) + except Exception as ex: + print(f" cannot enumerate: {ex}") + continue + for tri_idx, G in enumerate(triangulations, start=1): + if time.time() - start > time_budget_sec: + break + G_copy = G.copy() + G_copy.is_planar(set_embedding=True) + D = dual_of(G_copy) + D.is_planar(set_embedding=True) + for face in D.faces(): + if len(face) != 5: + continue + for i_red in range(5): + if time.time() - start > time_budget_sec: + break + res = apply_reduction(D, face, i_red, 9999) + if res is None: + continue + H_1 = res['H'] + n_col_h1, kc_h1 = num_kempe_classes(H_1) + if kc_h1 == 0: + continue + # enumerate all proper colorings of H_1 to vary phi_1 + edges_1, colorings_1 = proper_3_edge_colorings(H_1) + # try EVERY phi_1 (might be slow for large H_1) + max_kc_hf = 0 + h_final_seen = {} # signature -> classes + for phi_1 in colorings_1: + phi_1_dict = {frozenset((e[0], e[1])): c + for e, c in zip(edges_1, phi_1)} + H_final = run_algorithm_to_completion( + H_1, phi_1_dict, res['named']) + # signature = (|V|, |E|, sorted edge tuples) + sig = (H_final.order(), H_final.size()) + if sig in h_final_seen: + continue + _, kc_hf = num_kempe_classes(H_final) + h_final_seen[sig] = kc_hf + if kc_hf > max_kc_hf: + max_kc_hf = kc_hf + over = max_kc_hf > kc_h1 + flag = "*** OVER ***" if over else "ok" + print(f" n={n} tri#{tri_idx} face|{len(face)} i_red={i_red}: " + f"H_1 kc={kc_h1}, max H_t* kc over {len(h_final_seen)} " + f"distinct outputs = {max_kc_hf} {flag}") + if over: + violations.append((n, tri_idx, i_red, kc_h1, max_kc_hf)) + sys.stdout.flush() + break # first face only + + print() + if violations: + print(f"Counterexamples (#K(H_t*) > #K(H_1)): {len(violations)}") + for v in violations: + print(f" {v}") + else: + print("No counterexamples found within tested range.") + + +if __name__ == '__main__': + main() diff --git a/papers/dual_decomposition_minimal_counterexamples/experiments/draw_lift_to_Gprime.py b/papers/dual_decomposition_minimal_counterexamples/experiments/draw_lift_to_Gprime.py new file mode 100644 index 0000000..3c85cdf --- /dev/null +++ b/papers/dual_decomposition_minimal_counterexamples/experiments/draw_lift_to_Gprime.py @@ -0,0 +1,464 @@ +"""Lift the recoloured + bridged H_1 back to G' (dual of the n=14 +triangulation), producing a proper 3-edge-colouring of the modified G'. + +The modified G' = G' with: subdivisions Y_1, Y_2 of the two green witness +edges, plus a new red edge Y_1-Y_2. + +Run with: sage experiments/draw_lift_to_Gprime.py +""" +from sage.all import Graph +from sage.graphs.graph_generators import graphs +import matplotlib.pyplot as plt +import math +import os + + +def tutte_layout(G_sage, avoid_verts=None, iterations=300): + """Same Tutte barycentric layout as in draw_iterated_reduction_n14.py.""" + avoid = set(avoid_verts or ()) + candidates = [] + for face in G_sage.faces(): + verts = [u for (u, v) in face] + if not (set(verts) & avoid): + candidates.append(verts) + if not candidates: + outer = [u for (u, v) in max(G_sage.faces(), key=len)] + else: + outer = max(candidates, key=len) + n_outer = len(outer) + pos = {} + for k, v in enumerate(outer): + ang = 2 * math.pi * k / n_outer + math.pi / 2 + pos[v] = (math.cos(ang), math.sin(ang)) + interior = [v for v in G_sage.vertex_iterator() if v not in pos] + for v in interior: pos[v] = (0.0, 0.0) + for _ in range(iterations): + new_pos = dict(pos) + for v in interior: + nbrs = list(G_sage.neighbor_iterator(v)) + sx = sum(pos[w][0] for w in nbrs) / len(nbrs) + sy = sum(pos[w][1] for w in nbrs) / len(nbrs) + new_pos[v] = (sx, sy) + pos = new_pos + return pos + +OUT_DIR = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) + +C = ['#dc2626', '#16a34a', '#2563eb'] +DARK = '#374151' +HIGHLIGHT = '#fef3c7' + + +def dual_of(G): + G.is_planar(set_embedding=True) + faces = G.faces() + edge_to_faces = {} + for fi, face in enumerate(faces): + for u, v in face: + edge_to_faces.setdefault(frozenset((u, v)), []).append(fi) + return Graph( + [(fs[0], fs[1]) for fs in edge_to_faces.values() if len(fs) == 2], + multiedges=False, loops=False) + + +def proper_3_edge_colorings(G): + edges = list(G.edges(labels=False)) + n = len(edges) + adj = [[] for _ in range(n)] + for i in range(n): + u, v = edges[i][0], edges[i][1] + for j in range(i): + x, y = edges[j][0], edges[j][1] + if u in (x, y) or v in (x, y): + adj[i].append(j); adj[j].append(i) + coloring = [-1] * n + results = [] + + def back(k): + if k == n: + results.append(tuple(coloring)); return + for c in range(3): + if all(coloring[j] != c for j in adj[k]): + coloring[k] = c + back(k + 1) + coloring[k] = -1 + back(0) + return edges, results + + +def kempe_cycle_set(edges, col_list, start_idx, color_pair): + a, b = color_pair + if col_list[start_idx] not in (a, b): return set() + in_sub = set(i for i in range(len(edges)) if col_list[i] in (a, b)) + visited = {start_idx}; stack = [start_idx] + while stack: + cur = stack.pop() + u, v = edges[cur][0], edges[cur][1] + for j in in_sub: + if j in visited: continue + x, y = edges[j][0], edges[j][1] + if u in (x, y) or v in (x, y): + visited.add(j); stack.append(j) + return visited + + +def edge_idx(edges, e_frozen): + for i, e in enumerate(edges): + if frozenset((e[0], e[1])) == e_frozen: + return i + return None + + +def trace_kempe_cycle(edges, col_list, start_idx, color_pair): + cycle_set = kempe_cycle_set(edges, col_list, start_idx, color_pair) + incident_at = {} + for ei in cycle_set: + u, v = edges[ei][0], edges[ei][1] + incident_at.setdefault(u, []).append(ei) + incident_at.setdefault(v, []).append(ei) + start_u, start_v = edges[start_idx][0], edges[start_idx][1] + walk = [(start_idx, start_v)] + cur_e = start_idx + cur_leave = start_v + while True: + nbrs = incident_at[cur_leave] + if len(nbrs) != 2: break + nxt = nbrs[0] if nbrs[1] == cur_e else nbrs[1] + u2, v2 = edges[nxt][0], edges[nxt][1] + leave_next = v2 if u2 == cur_leave else u2 + if nxt == start_idx: break + walk.append((nxt, leave_next)) + cur_e = nxt + cur_leave = leave_next + return walk + + +def matches_chord_apex_kempe(edges, col, named): + idx = {role: edge_idx(edges, ns) for role, ns in named.items()} + if any(v is None for v in idx.values()): return False + c_spike = col[idx['spike']] + c_merged = col[idx['merged']] + if c_spike != c_merged: return False + c_s0 = col[idx['side_0']]; c_s1 = col[idx['side_1']] + kc0 = kempe_cycle_set(edges, col, idx['spike'], (c_spike, c_s0)) + if idx['side_0'] not in kc0 or idx['merged'] not in kc0: return False + kc1 = kempe_cycle_set(edges, col, idx['spike'], (c_spike, c_s1)) + if idx['side_1'] not in kc1 or idx['merged'] not in kc1: return False + return True + + +def apply_reduction(G, face, i, v_n_label): + boundary = [u for (u, v) in face] + if len(set(boundary)) != 5: return None + A = [] + for B_k in boundary: + outer = [w for w in G.neighbor_iterator(B_k) if w not in boundary] + if len(outer) != 1: return None + A.append(outer[0]) + if len(set(A)) != 5 or A[(i+3) % 5] == A[(i+4) % 5]: return None + H = G.copy() + for v in boundary: H.delete_vertex(v) + H.add_vertex(v_n_label) + side_0 = (v_n_label, A[i]) + spike = (v_n_label, A[(i+1) % 5]) + side_1 = (v_n_label, A[(i+2) % 5]) + merged = (A[(i+3) % 5], A[(i+4) % 5]) + H.add_edges([side_0, spike, side_1, merged]) + if H.has_multiple_edges() or H.has_loops(): return None + if not H.is_planar(set_embedding=True): return None + if not all(H.degree(v) == 3 for v in H.vertex_iterator()): return None + return { + 'H': H, 'A': A, 'boundary': boundary, 'face': face, 'i_red': i, + 'named': { + 'spike': frozenset(spike), + 'side_0': frozenset(side_0), + 'side_1': frozenset(side_1), + 'merged': frozenset(merged), + }, + } + + +def find_first_match(): + for G in graphs.triangulations(14, minimum_degree=5): + if not G.is_planar(set_embedding=True): continue + D = dual_of(G); D.is_planar(set_embedding=True) + for face in D.faces(): + if len(face) != 5: continue + for i_red in range(5): + res = apply_reduction(D, face, i_red, '__v_n_1__') + if res is None: continue + H, named = res['H'], res['named'] + edges, gen = proper_3_edge_colorings(H) + for col in gen: + if matches_chord_apex_kempe(edges, col, named): + coloring_dict = {frozenset((e[0], e[1])): c + for e, c in zip(edges, col)} + return G, D, res, H, coloring_dict + return None + + +def find_conj_witness(H, edges, col_list, named): + GREEN, BLUE = 1, 2 + merged_idx = edge_idx(edges, named['merged']) + kc_gb = kempe_cycle_set(edges, col_list, merged_idx, (GREEN, BLUE)) + if merged_idx not in kc_gb: return None + for face in H.faces(): + face_edge_ids = [] + for u, v in face: + ei = edge_idx(edges, frozenset((u, v))) + if ei is not None: + face_edge_ids.append(ei) + green_on_face_in_kc = [ei for ei in face_edge_ids + if col_list[ei] == GREEN + and ei in kc_gb + and ei != merged_idx] + if len(green_on_face_in_kc) >= 2: + return face, green_on_face_in_kc[0], green_on_face_in_kc[1], kc_gb + return None + + +def main(): + print("Setting up ...") + G14, D, red_info, H, coloring = find_first_match() + i_red = red_info['i_red'] + boundary_in_D = red_info['boundary'] + A_in_D = red_info['A'] + named_in_D = red_info['named'] + print(f" Found: i_red = {i_red}") + print(f" G' has |V|={D.order()}, |E|={D.size()}") + + # Relabel H so all vertices are integers + H_relabel_map = {v: i for i, v in enumerate(H.vertex_iterator())} + inv_relabel = {i: v for v, i in H_relabel_map.items()} + H.relabel(perm=H_relabel_map, inplace=True) + coloring = {frozenset(H_relabel_map[u] for u in e): c + for e, c in coloring.items()} + named_H = {role: frozenset(H_relabel_map[u] for u in e) + for role, e in named_in_D.items()} + + H.is_planar(set_embedding=True) + edges_H = list(H.edges(labels=False)) + col_list = [coloring[frozenset((u, v))] for (u, v) in edges_H] + witness = find_conj_witness(H, edges_H, col_list, named_H) + face_w, e1, e2, kc_gb = witness + e1_uv = tuple(edges_H[e1]); e2_uv = tuple(edges_H[e2]) + print(f" Witness in H_1 (relabeled): e1 = {e1_uv}, e2 = {e2_uv}") + + e1_D = (inv_relabel[e1_uv[0]], inv_relabel[e1_uv[1]]) + e2_D = (inv_relabel[e2_uv[0]], inv_relabel[e2_uv[1]]) + print(f" Witness in D labels: e1 = {e1_D}, e2 = {e2_D}") + + # Build modified G' + G_mod = D.copy() + max_label = max(v for v in D.vertices(sort=False) if isinstance(v, int)) + Y1 = max_label + 1 + Y2 = Y1 + 1 + G_mod.add_vertex(Y1); G_mod.add_vertex(Y2) + G_mod.delete_edge(e1_D); G_mod.delete_edge(e2_D) + G_mod.add_edges([(e1_D[0], Y1), (Y1, e1_D[1]), + (e2_D[0], Y2), (Y2, e2_D[1]), + (Y1, Y2)]) + assert G_mod.is_planar(set_embedding=True) + print(f" Modified G': |V|={G_mod.order()}, |E|={G_mod.size()}") + + # Trace Kempe cycle from merged + merged_idx = edge_idx(edges_H, named_H['merged']) + walk = trace_kempe_cycle(edges_H, col_list, merged_idx, (1, 2)) + walk_edges = [w[0] for w in walk] + leave_at = [w[1] for w in walk] + + # Map relabeled-H vertex -> D label if not v_n_1, else None + def H_to_D(v): + d = inv_relabel[v] + return d if d != '__v_n_1__' else None + + # Build new coloring on G_mod's edges. + # Step A: copy non-named, non-e1, non-e2, non-v_n_1 edges' original colors. + new_coloring = {} + named_H_set = set(named_H.values()) + for e_fs, c in coloring.items(): + if e_fs in named_H_set: continue + if e_fs == frozenset(e1_uv) or e_fs == frozenset(e2_uv): continue + u, v = tuple(e_fs) + du, dv = H_to_D(u), H_to_D(v) + if du is None or dv is None: continue + new_coloring[frozenset((du, dv))] = c + + # Step B: walk K' (subdivided cycle) starting from merged. + # For each old cycle edge that is NOT spike/side_0/side_1/merged + # (i.e., not involving v_n_1, not the chord), we OVERWRITE its color + # via the alternation. For e1, e2 we instead emit the two subdivision + # halves. For named edges (spike, side_1, merged), they don't exist + # in G_mod, so we record the would-be color to use later for f-vector. + pos = 0 + cycle_label = {} # e_fs in D labels -> new color (for cycle edges in G_mod) + half_label = {} # halves' colors + would_be = {} # named role -> would-be color after recoloring + for k, ei in enumerate(walk_edges): + leaving_vertex = leave_at[k] + u, v = edges_H[ei][0], edges_H[ei][1] + entry_vertex = v if leaving_vertex == u else u + e_fs_H = frozenset((u, v)) + if ei == e1: + c0 = 2 if pos % 2 == 0 else 1; pos += 1 + c1 = 2 if pos % 2 == 0 else 1; pos += 1 + half_label[frozenset((inv_relabel[entry_vertex], Y1))] = c0 + half_label[frozenset((Y1, inv_relabel[leaving_vertex]))] = c1 + elif ei == e2: + c0 = 2 if pos % 2 == 0 else 1; pos += 1 + c1 = 2 if pos % 2 == 0 else 1; pos += 1 + half_label[frozenset((inv_relabel[entry_vertex], Y2))] = c0 + half_label[frozenset((Y2, inv_relabel[leaving_vertex]))] = c1 + else: + c = 2 if pos % 2 == 0 else 1; pos += 1 + # is this a named edge (spike/side_1/merged)? Note: it can't be + # side_0 since side_0 is red and the cycle is green/blue. + for role, ef in named_H.items(): + if ef == e_fs_H: + would_be[role] = c + break + else: + # Regular cycle edge: convert to D labels + du, dv = H_to_D(u), H_to_D(v) + if du is None or dv is None: + # Shouldn't happen for non-named edges + pass + else: + cycle_label[frozenset((du, dv))] = c + + # Apply cycle relabeling + for e_fs, c in cycle_label.items(): + new_coloring[e_fs] = c + # Apply half colors + for e_fs, c in half_label.items(): + new_coloring[e_fs] = c + # New red edge + new_coloring[frozenset((Y1, Y2))] = 0 + + print(f" Would-be colors of named H_1 edges after recolor: {would_be}") + # would_be may not include side_0 (not on cycle); side_0's color is + # whatever it was in original (= red = 0). + if 'side_0' not in would_be: + would_be['side_0'] = coloring[named_H['side_0']] # 0 (red) + + # Step C: color the 5 externals f_k = B_k - A_k. + # At each A_k, the third color = would_be color of the missing H_1 edge. + def third(c1, c2): return ({0, 1, 2} - {c1, c2}).pop() + externals_colors = [None] * 5 + for k, B_k in enumerate(boundary_in_D): + A_k = A_in_D[k] + # Which named role was at A_k in H_1? + # A_in_D[i_red] = side_0's endpoint, A_in_D[i_red+1] = spike's, + # A_in_D[i_red+2] = side_1's, A_in_D[i_red+3,+4] = merged. + if k == i_red: role = 'side_0' + elif k == (i_red+1) % 5: role = 'spike' + elif k == (i_red+2) % 5: role = 'side_1' + else: role = 'merged' + c_ext = would_be[role] + new_coloring[frozenset((B_k, A_k))] = c_ext + externals_colors[k] = c_ext + print(f" f-vector at F_v: {externals_colors}") + + # Step D: 5 boundary edges B_k - B_{k+1} via Lemma 2.4. + boundary_colors = [None] * 5 + for k in range(5): + f_k = externals_colors[k] + f_kp1 = externals_colors[(k + 1) % 5] + if f_k != f_kp1: + boundary_colors[k] = third(f_k, f_kp1) + for _ in range(20): + changed = False + for k in range(5): + if boundary_colors[k] is not None: continue + f_k = externals_colors[k] + prev_c = boundary_colors[(k - 1) % 5] + next_c = boundary_colors[(k + 1) % 5] + forbidden = {f_k} + if prev_c is not None: forbidden.add(prev_c) + if next_c is not None: forbidden.add(next_c) + allowed = list({0, 1, 2} - forbidden) + if allowed: + boundary_colors[k] = allowed[0] + changed = True + if not changed: break + + for k in range(5): + if boundary_colors[k] is None: + print(f" WARNING: undetermined boundary color at k={k}") + return + B_k = boundary_in_D[k]; B_kp1 = boundary_in_D[(k + 1) % 5] + new_coloring[frozenset((B_k, B_kp1))] = boundary_colors[k] + + # Sanity check + bad = [] + for v in G_mod.vertices(sort=False): + seen = [] + for w in G_mod.neighbor_iterator(v): + seen.append(new_coloring.get(frozenset((v, w)))) + if None in seen or len(set(seen)) != len(seen): + bad.append((v, seen)) + if bad: + print(f" PROPRIETY FAILS at vertices:") + for v, s in bad[:5]: + print(f" {v}: {s}") + else: + print(" Propriety holds at every vertex of modified G'.") + + # Use H_1's Tutte layout for vertices shared between H_1 and G' (the 19 + # surviving vertices). Then add the 5 boundary vertices B_k of partial F_v + # by running a local barycenter iteration with the shared vertices fixed. + H.is_planar(set_embedding=True) + H_pos = tutte_layout(H, + avoid_verts={H_relabel_map['__v_n_1__']}) + # Map H_1 positions back to D labels (skip v_n_1) + pos_layout = {} + for v_H, p in H_pos.items(): + v_D = inv_relabel[v_H] + if v_D != '__v_n_1__': + pos_layout[v_D] = p + # Place B_k's by iterating barycenter of their 3 neighbours in G_mod + # (B_{k-1}, B_{k+1}, A_k); start each B_k near its A_k. + B_pos = {B_k: pos_layout[A_in_D[k]] + for k, B_k in enumerate(boundary_in_D)} + for _ in range(300): + new_B = {} + for k, B_k in enumerate(boundary_in_D): + B_prev = boundary_in_D[(k - 1) % 5] + B_next = boundary_in_D[(k + 1) % 5] + A_k = A_in_D[k] + sx = (B_pos[B_prev][0] + B_pos[B_next][0] + pos_layout[A_k][0]) / 3 + sy = (B_pos[B_prev][1] + B_pos[B_next][1] + pos_layout[A_k][1]) / 3 + new_B[B_k] = (sx, sy) + B_pos = new_B + for B_k, p in B_pos.items(): + pos_layout[B_k] = p + # Y_1, Y_2 at midpoints of their subdivided edges e1, e2 + pos_layout[Y1] = ((pos_layout[e1_D[0]][0] + pos_layout[e1_D[1]][0]) / 2, + (pos_layout[e1_D[0]][1] + pos_layout[e1_D[1]][1]) / 2) + pos_layout[Y2] = ((pos_layout[e2_D[0]][0] + pos_layout[e2_D[1]][0]) / 2, + (pos_layout[e2_D[0]][1] + pos_layout[e2_D[1]][1]) / 2) + + fig, ax = plt.subplots(figsize=(8, 8)) + for u, v, _ in G_mod.edges(): + e = frozenset((u, v)) + c = C[new_coloring[e]] + lw = 3.4 if e == frozenset((Y1, Y2)) else 1.5 + (x0, y0), (x1, y1) = pos_layout[u], pos_layout[v] + ax.plot([x0, x1], [y0, y1], color=c, lw=lw, zorder=2) + for v in G_mod.vertices(sort=False): + x, y = pos_layout[v] + if v in (Y1, Y2): + ax.scatter(x, y, s=140, color=DARK, edgecolors='white', + linewidths=1.6, zorder=6) + else: + ax.scatter(x, y, s=55, color=DARK, zorder=3) + ax.set_aspect('equal') + ax.axis('off') + out_path = os.path.join(OUT_DIR, 'fig_lift_to_Gprime.png') + fig.savefig(out_path, dpi=170, bbox_inches='tight') + plt.close(fig) + print(f"Wrote {out_path}") + + +if __name__ == '__main__': + main() diff --git a/papers/dual_decomposition_minimal_counterexamples/experiments/draw_step1_conj36.py b/papers/dual_decomposition_minimal_counterexamples/experiments/draw_step1_conj36.py new file mode 100644 index 0000000..3624d8c --- /dev/null +++ b/papers/dual_decomposition_minimal_counterexamples/experiments/draw_step1_conj36.py @@ -0,0 +1,277 @@ +"""Draw a Conjecture 3.6 witness: on H_1 with its chord-apex+Kempe coloring, +find a face with two green edges that lie (with the merged edge) on a common +{green, blue}-Kempe cycle. Subdivide both green edges with new vertices and +join the two new vertices by a new red edge. + +Run with: sage experiments/draw_step1_conj36.py +""" +from sage.all import Graph +from sage.graphs.graph_generators import graphs +import matplotlib.pyplot as plt +from matplotlib.patches import Polygon +import math +import os + +OUT_DIR = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) + +C = ['#dc2626', '#16a34a', '#2563eb'] # 0=red 1=green 2=blue +GRAY = '#9ca3af' +DARK = '#374151' +HIGHLIGHT = '#fef3c7' + + +def dual_of(G): + G.is_planar(set_embedding=True) + faces = G.faces() + edge_to_faces = {} + for fi, face in enumerate(faces): + for u, v in face: + edge_to_faces.setdefault(frozenset((u, v)), []).append(fi) + return Graph( + [(fs[0], fs[1]) for fs in edge_to_faces.values() if len(fs) == 2], + multiedges=False, loops=False) + + +def apply_reduction(G, face, i, v_n_label): + boundary = [u for (u, v) in face] + if len(set(boundary)) != 5: return None + A = [] + for B_k in boundary: + outer = [w for w in G.neighbor_iterator(B_k) if w not in boundary] + if len(outer) != 1: return None + A.append(outer[0]) + if len(set(A)) != 5 or A[(i+3) % 5] == A[(i+4) % 5]: return None + H = G.copy() + for v in boundary: H.delete_vertex(v) + H.add_vertex(v_n_label) + side_0 = (v_n_label, A[i]) + spike = (v_n_label, A[(i+1) % 5]) + side_1 = (v_n_label, A[(i+2) % 5]) + merged = (A[(i+3) % 5], A[(i+4) % 5]) + H.add_edges([side_0, spike, side_1, merged]) + if H.has_multiple_edges() or H.has_loops(): return None + if not H.is_planar(set_embedding=True): return None + if not all(H.degree(v) == 3 for v in H.vertex_iterator()): return None + return { + 'H': H, 'A': A, + 'named': { + 'spike': frozenset(spike), + 'side_0': frozenset(side_0), + 'side_1': frozenset(side_1), + 'merged': frozenset(merged), + }, + } + + +def proper_3_edge_colorings(G): + edges = list(G.edges(labels=False)) + n = len(edges) + adj = [[] for _ in range(n)] + for i in range(n): + u, v = edges[i][0], edges[i][1] + for j in range(i): + x, y = edges[j][0], edges[j][1] + if u in (x, y) or v in (x, y): + adj[i].append(j); adj[j].append(i) + coloring = [-1] * n + results = [] + + def back(k): + if k == n: + results.append(tuple(coloring)); return + for c in range(3): + if all(coloring[j] != c for j in adj[k]): + coloring[k] = c + back(k + 1) + coloring[k] = -1 + back(0) + return edges, results + + +def kempe_cycle(edges, coloring, start_idx, color_pair): + a, b = color_pair + if coloring[start_idx] not in (a, b): return set() + in_sub = set(i for i in range(len(edges)) if coloring[i] in (a, b)) + visited = {start_idx}; stack = [start_idx] + while stack: + cur = stack.pop() + u, v = edges[cur][0], edges[cur][1] + for j in in_sub: + if j in visited: continue + x, y = edges[j][0], edges[j][1] + if u in (x, y) or v in (x, y): + visited.add(j); stack.append(j) + return visited + + +def edge_idx(edges, e_frozen): + for i, e in enumerate(edges): + if frozenset((e[0], e[1])) == e_frozen: + return i + return None + + +def matches_chord_apex_kempe(edges, col, named): + idx = {role: edge_idx(edges, ns) for role, ns in named.items()} + if any(v is None for v in idx.values()): return False + c_spike = col[idx['spike']] + c_merged = col[idx['merged']] + if c_spike != c_merged: return False + c_s0 = col[idx['side_0']]; c_s1 = col[idx['side_1']] + kc0 = kempe_cycle(edges, col, idx['spike'], (c_spike, c_s0)) + if idx['side_0'] not in kc0 or idx['merged'] not in kc0: return False + kc1 = kempe_cycle(edges, col, idx['spike'], (c_spike, c_s1)) + if idx['side_1'] not in kc1 or idx['merged'] not in kc1: return False + return True + + +def find_first_match(): + for G in graphs.triangulations(14, minimum_degree=5): + if not G.is_planar(set_embedding=True): continue + D = dual_of(G); D.is_planar(set_embedding=True) + for face in D.faces(): + if len(face) != 5: continue + for i_red in range(5): + res = apply_reduction(D, face, i_red, '__v_n_1__') + if res is None: continue + H, named = res['H'], res['named'] + edges, gen = proper_3_edge_colorings(H) + for col in gen: + if matches_chord_apex_kempe(edges, col, named): + coloring_dict = {frozenset((e[0], e[1])): c + for e, c in zip(edges, col)} + return G, D, face, i_red, H, named, coloring_dict + return None + + +def tutte_layout(G_sage, avoid_verts=None, iterations=300): + avoid = set(avoid_verts or ()) + candidates = [] + for face in G_sage.faces(): + verts = [u for (u, v) in face] + if not (set(verts) & avoid): + candidates.append(verts) + if not candidates: + outer = [u for (u, v) in max(G_sage.faces(), key=len)] + else: + outer = max(candidates, key=len) + n_outer = len(outer) + pos = {} + for k, v in enumerate(outer): + ang = 2 * math.pi * k / n_outer + math.pi / 2 + pos[v] = (math.cos(ang), math.sin(ang)) + interior = [v for v in G_sage.vertex_iterator() if v not in pos] + for v in interior: pos[v] = (0.0, 0.0) + for _ in range(iterations): + new_pos = dict(pos) + for v in interior: + nbrs = list(G_sage.neighbor_iterator(v)) + sx = sum(pos[w][0] for w in nbrs) / len(nbrs) + sy = sum(pos[w][1] for w in nbrs) / len(nbrs) + new_pos[v] = (sx, sy) + pos = new_pos + return pos + + +def find_conj_witness(H, edges, col_list, named): + """Find a face F of H with two distinct green edges e1, e2, NEITHER equal + to the merged edge, such that e1, e2, merged all lie on the + {green, blue}-Kempe cycle through merged.""" + GREEN, BLUE = 1, 2 + merged_idx = edge_idx(edges, named['merged']) + kc_gb = kempe_cycle(edges, col_list, merged_idx, (GREEN, BLUE)) + if merged_idx not in kc_gb: + return None + for face in H.faces(): + face_edge_ids = [] + for u, v in face: + ei = edge_idx(edges, frozenset((u, v))) + if ei is not None: + face_edge_ids.append(ei) + green_on_face_in_kc = [ei for ei in face_edge_ids + if col_list[ei] == GREEN + and ei in kc_gb + and ei != merged_idx] + if len(green_on_face_in_kc) >= 2: + return face, green_on_face_in_kc[0], green_on_face_in_kc[1], kc_gb + return None + + +def main(): + print("Searching for the first n=14 chord-apex+Kempe match ...") + result = find_first_match() + G14, D, face_chosen, i_red, H, named, coloring = result + print(f" Found: i_red = {i_red}") + + H_relabel_map = {v: i for i, v in enumerate(H.vertex_iterator())} + H.relabel(perm=H_relabel_map, inplace=True) + vn = H_relabel_map['__v_n_1__'] + coloring = {frozenset(H_relabel_map[u] for u in e): c + for e, c in coloring.items()} + named = {role: frozenset(H_relabel_map[u] for u in e) + for role, e in named.items()} + + H.is_planar(set_embedding=True) + pos = tutte_layout(H, avoid_verts={vn}) + E_protected = set(named.values()) + + # Build (edges, coloring) in list/tuple form to use kempe helpers + edges = list(H.edges(labels=False)) + col_list = [coloring[frozenset((u, v))] for (u, v) in edges] + + witness = find_conj_witness(H, edges, col_list, named) + if witness is None: + print("ERROR: no witness found.") + return + face_w, e1, e2, kc_gb = witness + e1_uv = tuple(edges[e1]); e2_uv = tuple(edges[e2]) + print(f" Witness face has {len(face_w)} edges.") + print(f" e1 = {e1_uv}, e2 = {e2_uv}") + print(f" {{green, blue}}-Kempe cycle through merged: {len(kc_gb)} edges.") + + # Midpoints in the layout + mp1 = ((pos[e1_uv[0]][0] + pos[e1_uv[1]][0]) / 2, + (pos[e1_uv[0]][1] + pos[e1_uv[1]][1]) / 2) + mp2 = ((pos[e2_uv[0]][0] + pos[e2_uv[1]][0]) / 2, + (pos[e2_uv[0]][1] + pos[e2_uv[1]][1]) / 2) + + # Draw + fig, ax = plt.subplots(figsize=(8, 8)) + for u, v, _ in H.edges(): + e = frozenset([u, v]) + c = C[coloring[e]] + lw = 3.8 if e in E_protected else 1.4 + (x0, y0), (x1, y1) = pos[u], pos[v] + ax.plot([x0, x1], [y0, y1], color=c, lw=lw, zorder=2) + for v in H.vertices(sort=False): + x, y = pos[v] + if v == vn: + ax.scatter(x, y, s=320, color=HIGHLIGHT, marker='s', + edgecolors='black', linewidths=1.2, zorder=4) + ax.annotate('$v_n^{(1)}$', (x, y), + textcoords='offset points', xytext=(16, 16), + ha='left', fontsize=14, fontweight='bold', + color=DARK, zorder=6, + bbox=dict(boxstyle='round,pad=0.2', fc='white', + ec=DARK, lw=0.6)) + else: + ax.scatter(x, y, s=70, color=DARK, zorder=3) + + # New red edge between midpoints + ax.plot([mp1[0], mp2[0]], [mp1[1], mp2[1]], + color=C[0], lw=4.0, zorder=5) + # New vertices + for (mx, my) in (mp1, mp2): + ax.scatter(mx, my, s=130, color=DARK, edgecolors='white', + linewidths=1.6, zorder=6) + + ax.set_aspect('equal') + ax.axis('off') + out_path = os.path.join(OUT_DIR, 'fig_alg_step1_conj36.png') + fig.savefig(out_path, dpi=170, bbox_inches='tight') + plt.close(fig) + print(f"Wrote {out_path}") + + +if __name__ == '__main__': + main() diff --git a/papers/dual_decomposition_minimal_counterexamples/experiments/draw_step1_conj36_recolored.py b/papers/dual_decomposition_minimal_counterexamples/experiments/draw_step1_conj36_recolored.py new file mode 100644 index 0000000..02699a2 --- /dev/null +++ b/papers/dual_decomposition_minimal_counterexamples/experiments/draw_step1_conj36_recolored.py @@ -0,0 +1,373 @@ +"""Build the Conjecture 3.6 witness on H_1, subdivide the two green edges +with new vertices X1, X2, add a new red edge X1-X2, then recolor the +{green, blue}-Kempe cycle through merged so that walking it from merged +gives the alternating sequence blue, green, blue, green, ... (equivalently, +a Kempe swap of green/blue along the cycle). + +Edges off the cycle keep their original colour; the new red edge stays red. +Propriety holds throughout: at every old vertex the 2 cycle edges still +alternate green/blue and the off-cycle edge is red; at X1 and X2 the two +cycle halves are forced to opposite colours of {green, blue} and the new +red edge supplies the third colour. + +Run with: sage experiments/draw_step1_conj36_recolored.py +""" +from sage.all import Graph +from sage.graphs.graph_generators import graphs +import matplotlib.pyplot as plt +from matplotlib.patches import Polygon +import math +import os + +OUT_DIR = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) + +C = ['#dc2626', '#16a34a', '#2563eb'] # 0=red 1=green 2=blue +GRAY = '#9ca3af' +DARK = '#374151' +HIGHLIGHT = '#fef3c7' + + +def dual_of(G): + G.is_planar(set_embedding=True) + faces = G.faces() + edge_to_faces = {} + for fi, face in enumerate(faces): + for u, v in face: + edge_to_faces.setdefault(frozenset((u, v)), []).append(fi) + return Graph( + [(fs[0], fs[1]) for fs in edge_to_faces.values() if len(fs) == 2], + multiedges=False, loops=False) + + +def apply_reduction(G, face, i, v_n_label): + boundary = [u for (u, v) in face] + if len(set(boundary)) != 5: return None + A = [] + for B_k in boundary: + outer = [w for w in G.neighbor_iterator(B_k) if w not in boundary] + if len(outer) != 1: return None + A.append(outer[0]) + if len(set(A)) != 5 or A[(i+3) % 5] == A[(i+4) % 5]: return None + H = G.copy() + for v in boundary: H.delete_vertex(v) + H.add_vertex(v_n_label) + side_0 = (v_n_label, A[i]) + spike = (v_n_label, A[(i+1) % 5]) + side_1 = (v_n_label, A[(i+2) % 5]) + merged = (A[(i+3) % 5], A[(i+4) % 5]) + H.add_edges([side_0, spike, side_1, merged]) + if H.has_multiple_edges() or H.has_loops(): return None + if not H.is_planar(set_embedding=True): return None + if not all(H.degree(v) == 3 for v in H.vertex_iterator()): return None + return { + 'H': H, 'A': A, + 'named': { + 'spike': frozenset(spike), + 'side_0': frozenset(side_0), + 'side_1': frozenset(side_1), + 'merged': frozenset(merged), + }, + } + + +def proper_3_edge_colorings(G): + edges = list(G.edges(labels=False)) + n = len(edges) + adj = [[] for _ in range(n)] + for i in range(n): + u, v = edges[i][0], edges[i][1] + for j in range(i): + x, y = edges[j][0], edges[j][1] + if u in (x, y) or v in (x, y): + adj[i].append(j); adj[j].append(i) + coloring = [-1] * n + results = [] + + def back(k): + if k == n: + results.append(tuple(coloring)); return + for c in range(3): + if all(coloring[j] != c for j in adj[k]): + coloring[k] = c + back(k + 1) + coloring[k] = -1 + back(0) + return edges, results + + +def kempe_cycle_edges(edges, col_list, start_idx, color_pair): + a, b = color_pair + if col_list[start_idx] not in (a, b): return set() + in_sub = set(i for i in range(len(edges)) if col_list[i] in (a, b)) + visited = {start_idx}; stack = [start_idx] + while stack: + cur = stack.pop() + u, v = edges[cur][0], edges[cur][1] + for j in in_sub: + if j in visited: continue + x, y = edges[j][0], edges[j][1] + if u in (x, y) or v in (x, y): + visited.add(j); stack.append(j) + return visited + + +def edge_idx(edges, e_frozen): + for i, e in enumerate(edges): + if frozenset((e[0], e[1])) == e_frozen: + return i + return None + + +def trace_kempe_cycle(edges, col_list, start_idx, color_pair): + """Walk the (a,b)-Kempe cycle through edges[start_idx]. Returns a list + of (edge_idx, direction) where direction is the vertex you LEAVE the + edge by. The returned list is in cyclic order, length 2L.""" + a, b = color_pair + cycle_edges = kempe_cycle_edges(edges, col_list, start_idx, color_pair) + # build adjacency: at each vertex on the cycle, the 2 (a,b)-edges incident + incident_at = {} + for ei in cycle_edges: + u, v = edges[ei][0], edges[ei][1] + incident_at.setdefault(u, []).append(ei) + incident_at.setdefault(v, []).append(ei) + # walk + start_u, start_v = edges[start_idx][0], edges[start_idx][1] + walk = [(start_idx, start_v)] + cur_e = start_idx + cur_leave = start_v + while True: + # at cur_leave, the 2 cycle edges are cur_e and the next one + nbrs = incident_at[cur_leave] + if len(nbrs) != 2: break + nxt = nbrs[0] if nbrs[1] == cur_e else nbrs[1] + u2, v2 = edges[nxt][0], edges[nxt][1] + leave_next = v2 if u2 == cur_leave else u2 + if nxt == start_idx: break + walk.append((nxt, leave_next)) + cur_e = nxt + cur_leave = leave_next + return walk + + +def matches_chord_apex_kempe(edges, col, named): + idx = {role: edge_idx(edges, ns) for role, ns in named.items()} + if any(v is None for v in idx.values()): return False + c_spike = col[idx['spike']] + c_merged = col[idx['merged']] + if c_spike != c_merged: return False + c_s0 = col[idx['side_0']]; c_s1 = col[idx['side_1']] + kc0 = kempe_cycle_edges(edges, col, idx['spike'], (c_spike, c_s0)) + if idx['side_0'] not in kc0 or idx['merged'] not in kc0: return False + kc1 = kempe_cycle_edges(edges, col, idx['spike'], (c_spike, c_s1)) + if idx['side_1'] not in kc1 or idx['merged'] not in kc1: return False + return True + + +def find_first_match(): + for G in graphs.triangulations(14, minimum_degree=5): + if not G.is_planar(set_embedding=True): continue + D = dual_of(G); D.is_planar(set_embedding=True) + for face in D.faces(): + if len(face) != 5: continue + for i_red in range(5): + res = apply_reduction(D, face, i_red, '__v_n_1__') + if res is None: continue + H, named = res['H'], res['named'] + edges, gen = proper_3_edge_colorings(H) + for col in gen: + if matches_chord_apex_kempe(edges, col, named): + coloring_dict = {frozenset((e[0], e[1])): c + for e, c in zip(edges, col)} + return G, D, face, i_red, H, named, coloring_dict + return None + + +def tutte_layout(G_sage, avoid_verts=None, iterations=300): + avoid = set(avoid_verts or ()) + candidates = [] + for face in G_sage.faces(): + verts = [u for (u, v) in face] + if not (set(verts) & avoid): + candidates.append(verts) + if not candidates: + outer = [u for (u, v) in max(G_sage.faces(), key=len)] + else: + outer = max(candidates, key=len) + n_outer = len(outer) + pos = {} + for k, v in enumerate(outer): + ang = 2 * math.pi * k / n_outer + math.pi / 2 + pos[v] = (math.cos(ang), math.sin(ang)) + interior = [v for v in G_sage.vertex_iterator() if v not in pos] + for v in interior: pos[v] = (0.0, 0.0) + for _ in range(iterations): + new_pos = dict(pos) + for v in interior: + nbrs = list(G_sage.neighbor_iterator(v)) + sx = sum(pos[w][0] for w in nbrs) / len(nbrs) + sy = sum(pos[w][1] for w in nbrs) / len(nbrs) + new_pos[v] = (sx, sy) + pos = new_pos + return pos + + +def find_conj_witness(H, edges, col_list, named): + GREEN, BLUE = 1, 2 + merged_idx = edge_idx(edges, named['merged']) + kc_gb = kempe_cycle_edges(edges, col_list, merged_idx, (GREEN, BLUE)) + if merged_idx not in kc_gb: + return None + for face in H.faces(): + face_edge_ids = [] + for u, v in face: + ei = edge_idx(edges, frozenset((u, v))) + if ei is not None: + face_edge_ids.append(ei) + green_on_face_in_kc = [ei for ei in face_edge_ids + if col_list[ei] == GREEN + and ei in kc_gb + and ei != merged_idx] + if len(green_on_face_in_kc) >= 2: + return face, green_on_face_in_kc[0], green_on_face_in_kc[1], kc_gb + return None + + +def main(): + print("Setting up ...") + result = find_first_match() + G14, D, face_chosen, i_red, H, named, coloring = result + print(f" Found: i_red = {i_red}") + + H_relabel_map = {v: i for i, v in enumerate(H.vertex_iterator())} + H.relabel(perm=H_relabel_map, inplace=True) + vn = H_relabel_map['__v_n_1__'] + coloring = {frozenset(H_relabel_map[u] for u in e): c + for e, c in coloring.items()} + named = {role: frozenset(H_relabel_map[u] for u in e) + for role, e in named.items()} + + H.is_planar(set_embedding=True) + pos = tutte_layout(H, avoid_verts={vn}) + + edges = list(H.edges(labels=False)) + col_list = [coloring[frozenset((u, v))] for (u, v) in edges] + + witness = find_conj_witness(H, edges, col_list, named) + face_w, e1, e2, kc_gb = witness + e1_uv = tuple(edges[e1]); e2_uv = tuple(edges[e2]) + merged_idx = edge_idx(edges, named['merged']) + print(f" Witness: e1 = {e1_uv}, e2 = {e2_uv}, |kc_gb| = {len(kc_gb)}") + + # Trace the Kempe cycle starting from merged + walk = trace_kempe_cycle(edges, col_list, merged_idx, (1, 2)) + walk_edges_in_order = [w[0] for w in walk] + leave_in_order = [w[1] for w in walk] + print(f" Kempe cycle (in order from merged): length {len(walk_edges_in_order)}") + + # Compute midpoints + mp1 = ((pos[e1_uv[0]][0] + pos[e1_uv[1]][0]) / 2, + (pos[e1_uv[0]][1] + pos[e1_uv[1]][1]) / 2) + mp2 = ((pos[e2_uv[0]][0] + pos[e2_uv[1]][0]) / 2, + (pos[e2_uv[0]][1] + pos[e2_uv[1]][1]) / 2) + + # Construct the new graph: H with e1, e2 subdivided and new red edge X1-X2. + H_new = H.copy() + X1 = max(H.vertices(sort=False)) + 1 + X2 = X1 + 1 + H_new.add_vertex(X1); H_new.add_vertex(X2) + H_new.delete_edge(e1_uv) + H_new.delete_edge(e2_uv) + e1_a, e1_b = e1_uv + e2_a, e2_b = e2_uv + H_new.add_edges([(e1_a, X1), (X1, e1_b), + (e2_a, X2), (X2, e2_b), + (X1, X2)]) + pos_new = dict(pos); pos_new[X1] = mp1; pos_new[X2] = mp2 + + # Build subdivided cycle K' as a list of (edge_frozenset, "entry vertex + # in original direction") in cyclic order starting from merged. + K_prime = [] + for k, ei in enumerate(walk_edges_in_order): + leaving_vertex = leave_in_order[k] + u, v = edges[ei][0], edges[ei][1] + entry_vertex = v if leaving_vertex == u else u + if ei == e1: + K_prime.append(frozenset((entry_vertex, X1))) + K_prime.append(frozenset((X1, leaving_vertex))) + elif ei == e2: + K_prime.append(frozenset((entry_vertex, X2))) + K_prime.append(frozenset((X2, leaving_vertex))) + else: + K_prime.append(frozenset((u, v))) + + print(f" Subdivided cycle length: {len(K_prime)}") + + # Recolor K' alternately starting from merged = blue + new_coloring = dict(coloring) + new_coloring.pop(frozenset(e1_uv), None) + new_coloring.pop(frozenset(e2_uv), None) + for k, e_fs in enumerate(K_prime): + new_coloring[e_fs] = 2 if k % 2 == 0 else 1 # blue, green, blue, green + # New red edge X1-X2 + new_coloring[frozenset((X1, X2))] = 0 + + # Sanity: check propriety at every vertex of H_new + bad = False + for v in H_new.vertices(sort=False): + seen = [] + for w in H_new.neighbor_iterator(v): + seen.append(new_coloring[frozenset((v, w))]) + if len(set(seen)) != len(seen): + print(f" *** propriety FAILS at vertex {v}: colors {seen}") + bad = True + if not bad: + print(" Propriety holds at every vertex.") + + # Identify which edges of H_new are "protected" (the original named edges, + # minus e1, e2 which have been subdivided away). + E_protected = set() + for role, ef in named.items(): + if ef in (frozenset(e1_uv), frozenset(e2_uv)): + continue + E_protected.add(ef) + + # Draw + fig, ax = plt.subplots(figsize=(8, 8)) + for u, v, _ in H_new.edges(): + e = frozenset([u, v]) + c = C[new_coloring[e]] + if e == frozenset((X1, X2)): + lw = 4.0 + elif e in E_protected: + lw = 3.8 + else: + lw = 1.4 + (x0, y0), (x1, y1) = pos_new[u], pos_new[v] + ax.plot([x0, x1], [y0, y1], color=c, lw=lw, zorder=2) + for v in H_new.vertices(sort=False): + x, y = pos_new[v] + if v == vn: + ax.scatter(x, y, s=320, color=HIGHLIGHT, marker='s', + edgecolors='black', linewidths=1.2, zorder=4) + ax.annotate('$v_n^{(1)}$', (x, y), + textcoords='offset points', xytext=(16, 16), + ha='left', fontsize=14, fontweight='bold', + color=DARK, zorder=6, + bbox=dict(boxstyle='round,pad=0.2', fc='white', + ec=DARK, lw=0.6)) + elif v in (X1, X2): + ax.scatter(x, y, s=130, color=DARK, edgecolors='white', + linewidths=1.6, zorder=6) + else: + ax.scatter(x, y, s=70, color=DARK, zorder=3) + + ax.set_aspect('equal') + ax.axis('off') + out_path = os.path.join(OUT_DIR, 'fig_alg_step1_conj36_recolored.png') + fig.savefig(out_path, dpi=170, bbox_inches='tight') + plt.close(fig) + print(f"Wrote {out_path}") + + +if __name__ == '__main__': + main() diff --git a/papers/dual_decomposition_minimal_counterexamples/experiments/search_conj_3_6_counterexample.py b/papers/dual_decomposition_minimal_counterexamples/experiments/search_conj_3_6_counterexample.py new file mode 100644 index 0000000..d1d684a --- /dev/null +++ b/papers/dual_decomposition_minimal_counterexamples/experiments/search_conj_3_6_counterexample.py @@ -0,0 +1,380 @@ +"""Search for a counterexample to Conjecture 3.6. + +For each min-deg-5 triangulation G and each reduced dual H_1, find a proper +3-edge-coloring phi_1 of H_1 that satisfies (i) chord-apex (spike = merged) +and (ii) both Kempe-chain conditions of Lemma 2.7 -- i.e., the kind of +coloring that a minimal counterexample's reduced dual would be forced to +have. Run Algorithm 3.1 to completion from phi_1, get the final colouring +phi_t* on H_t*. Then enumerate all proper 3-edge-colorings of H_t*, find the +Kempe class containing phi_t*, and check whether any coloring in that class +is "all-distinct" (every spike_t != merged_t for t = 1, ..., t*). + +If no such all-distinct coloring exists in phi_t*'s Kempe class: +counterexample to Conjecture 3.6 found. + +Run with: sage experiments/search_conj_3_6_counterexample.py +""" +from sage.all import Graph +from sage.graphs.graph_generators import graphs +import sys +import time + + +def dual_of(G): + G.is_planar(set_embedding=True) + faces = G.faces() + edge_to_faces = {} + for fi, face in enumerate(faces): + for u, v in face: + edge_to_faces.setdefault(frozenset((u, v)), []).append(fi) + dual_edges = [(fs[0], fs[1]) for fs in edge_to_faces.values() if len(fs) == 2] + return Graph(dual_edges, multiedges=False, loops=False) + + +def apply_reduction(G, face, i, v_n_label): + boundary = [u for (u, v) in face] + if len(set(boundary)) != 5: + return None + A = [] + for B_k in boundary: + outer = [w for w in G.neighbor_iterator(B_k) if w not in boundary] + if len(outer) != 1: + return None + A.append(outer[0]) + if len(set(A)) != 5: + return None + if A[(i + 3) % 5] == A[(i + 4) % 5]: + return None + H = G.copy() + for v in boundary: + H.delete_vertex(v) + H.add_vertex(v_n_label) + side_0 = (v_n_label, A[i]) + spike = (v_n_label, A[(i + 1) % 5]) + side_1 = (v_n_label, A[(i + 2) % 5]) + merged = (A[(i + 3) % 5], A[(i + 4) % 5]) + H.add_edges([side_0, spike, side_1, merged]) + if H.has_multiple_edges() or H.has_loops(): + return None + if not H.is_planar(set_embedding=True): + return None + if not all(H.degree(v) == 3 for v in H.vertex_iterator()): + return None + return { + 'H': H, 'A': A, 'boundary': boundary, + 'named': { + 'spike': frozenset(spike), + 'side_0': frozenset(side_0), + 'side_1': frozenset(side_1), + 'merged': frozenset(merged), + }, + } + + +def proper_3_edge_colorings(G): + edges = list(G.edges(labels=False)) + n = len(edges) + adj = [[] for _ in range(n)] + for i in range(n): + u, v = edges[i][0], edges[i][1] + for j in range(i): + x, y = edges[j][0], edges[j][1] + if u in (x, y) or v in (x, y): + adj[i].append(j) + adj[j].append(i) + coloring = [-1] * n + results = [] + + def back(k): + if k == n: + results.append(tuple(coloring)) + return + for c in range(3): + if all(coloring[j] != c for j in adj[k]): + coloring[k] = c + back(k + 1) + coloring[k] = -1 + + back(0) + return edges, results + + +def edge_idx(edges, e_frozen): + for i, e in enumerate(edges): + if frozenset((e[0], e[1])) == e_frozen: + return i + return None + + +def kempe_cycle(edges, coloring, start_idx, color_pair): + a, b = color_pair + if coloring[start_idx] not in (a, b): + return set() + in_sub = set(i for i in range(len(edges)) if coloring[i] in (a, b)) + visited = {start_idx} + stack = [start_idx] + while stack: + cur = stack.pop() + u, v = edges[cur][0], edges[cur][1] + for j in in_sub: + if j in visited: + continue + x, y = edges[j][0], edges[j][1] + if u in (x, y) or v in (x, y): + visited.add(j) + stack.append(j) + return visited + + +def matches_chord_apex_kempe(edges, col, named): + idx = {role: edge_idx(edges, ns) for role, ns in named.items()} + if any(v is None for v in idx.values()): + return False + c_spike = col[idx['spike']] + c_merged = col[idx['merged']] + if c_spike != c_merged: + return False + c_s0 = col[idx['side_0']] + c_s1 = col[idx['side_1']] + kc0 = kempe_cycle(edges, col, idx['spike'], (c_spike, c_s0)) + if idx['side_0'] not in kc0 or idx['merged'] not in kc0: + return False + kc1 = kempe_cycle(edges, col, idx['spike'], (c_spike, c_s1)) + if idx['side_1'] not in kc1 or idx['merged'] not in kc1: + return False + return True + + +def find_safe_pentagonal_face(G, protected): + for face in G.faces(): + if len(face) != 5: + continue + boundary = [u for (u, v) in face] + boundary_edges = [frozenset([u, v]) for (u, v) in face] + externals = [] + A = [] + ok = True + for B_k in boundary: + outer = [w for w in G.neighbor_iterator(B_k) if w not in boundary] + if len(outer) != 1: + ok = False + break + externals.append(frozenset([B_k, outer[0]])) + A.append(outer[0]) + if not ok: + continue + if any(e in protected for e in boundary_edges + externals): + continue + return boundary, externals, A + return None + + +def valid_index(f_vec, A): + for i in range(5): + if f_vec[(i + 3) % 5] != f_vec[(i + 4) % 5]: + continue + if len({f_vec[i], f_vec[(i + 1) % 5], f_vec[(i + 2) % 5]}) != 3: + continue + if A[(i + 3) % 5] == A[(i + 4) % 5]: + continue + return i + return None + + +def run_algorithm_to_completion(H, coloring_dict, named_step1, vn_start=1000): + """Returns (H_final, coloring_final, list_of_named_dicts).""" + H = H.copy() + coloring = dict(coloring_dict) + all_named = [named_step1] + E = set(named_step1.values()) + next_vn = vn_start + + while True: + H.is_planar(set_embedding=True) + result = find_safe_pentagonal_face(H, E) + if result is None: + break + boundary, externals, A = result + f_vec = [coloring[e] for e in externals] + i_t = valid_index(f_vec, A) + if i_t is None: + break + v_n = next_vn + next_vn += 1 + H_new = H.copy() + for v in boundary: + H_new.delete_vertex(v) + H_new.add_vertex(v_n) + side_0 = (v_n, A[i_t]) + spike = (v_n, A[(i_t + 1) % 5]) + side_1 = (v_n, A[(i_t + 2) % 5]) + merged = (A[(i_t + 3) % 5], A[(i_t + 4) % 5]) + H_new.add_edges([side_0, spike, side_1, merged]) + if H_new.has_multiple_edges() or H_new.has_loops(): + break + if not H_new.is_planar(set_embedding=True): + break + H = H_new + coloring = {e: c for e, c in coloring.items() + if not any(u in boundary for u in e)} + coloring[frozenset(side_0)] = f_vec[i_t] + coloring[frozenset(spike)] = f_vec[(i_t + 1) % 5] + coloring[frozenset(side_1)] = f_vec[(i_t + 2) % 5] + coloring[frozenset(merged)] = f_vec[(i_t + 3) % 5] + named = { + 'spike': frozenset(spike), + 'side_0': frozenset(side_0), + 'side_1': frozenset(side_1), + 'merged': frozenset(merged), + } + E |= set(named.values()) + all_named.append(named) + return H, coloring, all_named + + +def kempe_class_via_union_find(edges, colorings): + """For each coloring, attempt every Kempe swap and union. Returns parent + array of disjoint-set forest.""" + n = len(colorings) + parent = list(range(n)) + + def find(x): + while parent[x] != x: + parent[x] = parent[parent[x]] + x = parent[x] + return x + + def union(x, y): + rx, ry = find(x), find(y) + if rx != ry: + parent[rx] = ry + + col_idx = {c: i for i, c in enumerate(colorings)} + for c_idx, col in enumerate(colorings): + for pair in [(0, 1), (0, 2), (1, 2)]: + visited = set() + for start in range(len(edges)): + if col[start] not in pair or start in visited: + continue + cyc = kempe_cycle(edges, col, start, pair) + visited |= cyc + a, b = pair + new_col = list(col) + for k in cyc: + if new_col[k] == a: + new_col[k] = b + elif new_col[k] == b: + new_col[k] = a + new_col = tuple(new_col) + if new_col != col and new_col in col_idx: + union(c_idx, col_idx[new_col]) + return [find(i) for i in range(n)] + + +def is_all_distinct(edges, col, all_named): + for named in all_named: + i_spike = edge_idx(edges, named['spike']) + i_merged = edge_idx(edges, named['merged']) + if i_spike is None or i_merged is None: + return False + if col[i_spike] == col[i_merged]: + return False + return True + + +def check_one_triangulation(G, n, idx_label, time_budget): + G_planar = G.is_planar(set_embedding=True) + if not G_planar: + return None + D = dual_of(G) + D.is_planar(set_embedding=True) + for face in D.faces(): + if len(face) != 5: + continue + for i_red in range(5): + res = apply_reduction(D, face, i_red, 999) + if res is None: + continue + H_1, named_1 = res['H'], res['named'] + edges_1, colorings_1 = proper_3_edge_colorings(H_1) + candidates = [col for col in colorings_1 + if matches_chord_apex_kempe(edges_1, col, named_1)] + if not candidates: + continue + # For the first candidate, run algorithm and check. + phi_1 = candidates[0] + coloring_dict = {frozenset((e[0], e[1])): c + for e, c in zip(edges_1, phi_1)} + H_final, phi_final_dict, all_named = run_algorithm_to_completion( + H_1, coloring_dict, named_1) + edges_final, colorings_final = proper_3_edge_colorings(H_final) + # find phi_final as a tuple + phi_final = tuple( + phi_final_dict[frozenset((e[0], e[1]))] for e in edges_final + ) + if phi_final not in colorings_final: + # not in enumeration, skip + continue + print(f" n={n}, tri#{idx_label}, face_size={len(face)}, " + f"i_red={i_red}: H_1 has {len(candidates)} chord+Kempe " + f"colorings; algorithm produced H_t* with |V|={H_final.order()}, " + f"|E|={H_final.size()}; H_t* has {len(colorings_final)} " + f"proper colorings.") + # Kempe classes + parent = kempe_class_via_union_find(edges_final, colorings_final) + phi_final_idx = colorings_final.index(phi_final) + phi_class = parent[phi_final_idx] + n_in_class = sum(1 for p in parent if p == phi_class) + print(f" phi_final's Kempe class has {n_in_class} colorings; " + f"total classes: {len(set(parent))}") + # search for all-distinct in same class + for ci, p in enumerate(parent): + if p != phi_class: + continue + if is_all_distinct(edges_final, colorings_final[ci], all_named): + print(f" found all-distinct coloring in same Kempe " + f"class -- Conj 3.6 holds for this instance.") + break + else: + print(f" *** NO all-distinct coloring in phi_final's " + f"Kempe class -- CONJECTURE 3.6 FAILS HERE ***") + return { + 'n': n, 'tri': idx_label, 'face_size': len(face), + 'i_red': i_red, 'H_final': H_final, + 'phi_final': phi_final, 'all_named': all_named, + } + return None + + +def main(max_n=16, time_budget_sec=600): + start = time.time() + for n in range(12, max_n + 1): + elapsed = time.time() - start + if elapsed > time_budget_sec: + print(f"\nTime budget {time_budget_sec}s exhausted at n={n}.") + return + print(f"\n=== n = {n} (elapsed {elapsed:.1f}s) ===") + try: + it = graphs.triangulations(n, minimum_degree=5) + except Exception as ex: + print(f" cannot enumerate: {ex}") + continue + for idx, G in enumerate(it, start=1): + if time.time() - start > time_budget_sec: + print(f"Time budget exhausted mid-n={n}.") + return + hit = check_one_triangulation(G, n, idx, + time_budget_sec - (time.time() - start)) + if hit is not None: + print() + print(f"=== Counterexample to Conjecture 3.6 ===") + print(f" n = {hit['n']}, triangulation #{hit['tri']}, " + f"i_red = {hit['i_red']}") + print(f" H_t* has |V|={hit['H_final'].order()}, " + f"|E|={hit['H_final'].size()}") + return + sys.stdout.flush() + + +if __name__ == '__main__': + main() diff --git a/papers/dual_decomposition_minimal_counterexamples/fig_alg_step1_conj36.png b/papers/dual_decomposition_minimal_counterexamples/fig_alg_step1_conj36.png new file mode 100644 index 0000000..29231f4 Binary files /dev/null and b/papers/dual_decomposition_minimal_counterexamples/fig_alg_step1_conj36.png differ diff --git a/papers/dual_decomposition_minimal_counterexamples/fig_alg_step1_conj36_recolored.png b/papers/dual_decomposition_minimal_counterexamples/fig_alg_step1_conj36_recolored.png new file mode 100644 index 0000000..da1e98e Binary files /dev/null and b/papers/dual_decomposition_minimal_counterexamples/fig_alg_step1_conj36_recolored.png differ diff --git a/papers/dual_decomposition_minimal_counterexamples/fig_lift_to_Gprime.png b/papers/dual_decomposition_minimal_counterexamples/fig_lift_to_Gprime.png new file mode 100644 index 0000000..f135f2f Binary files /dev/null and b/papers/dual_decomposition_minimal_counterexamples/fig_lift_to_Gprime.png differ diff --git a/papers/dual_decomposition_minimal_counterexamples/paper.aux b/papers/dual_decomposition_minimal_counterexamples/paper.aux index 3c47f89..95a65b0 100644 --- a/papers/dual_decomposition_minimal_counterexamples/paper.aux +++ b/papers/dual_decomposition_minimal_counterexamples/paper.aux @@ -17,12 +17,14 @@ \newlabel{alg:iterated-reduction}{{3.1}{7}} \newlabel{rem:alg-invariants}{{3.2}{7}} \newlabel{rem:alg-chord-apex}{{3.3}{7}} +\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Algorithm\nonbreakingspace 3.1\hbox {} on $G'=\mathrm {dual}(G)$, where $G$ is the first min-degree-$5$ plantri triangulation on $14$ vertices and $\varphi _1$ is a specific proper $3$-edge-colouring of $H_1$ that satisfies both the chord-apex condition (Lemma\nonbreakingspace 2.6\hbox {}) and the Kempe-cycle condition (Lemma\nonbreakingspace 2.7\hbox {}), found by \texttt {experiments/search\_kempe\_property.py}. \emph {Left:} $G'$ ($24$ vertices, $36$ edges) with the chosen pentagonal face shaded. \emph {Centre:} $H_1$ ($20$ vertices, $30$ edges) after step\nonbreakingspace (1) with $i_1 = 1$, $3$-edge-coloured by $\varphi _1$; the four edges around $v_n^{(1)}$ in $E$ are drawn thicker, and the spike and merged edges share the colour green. \emph {Right:} $H_2$ ($16$ vertices, $24$ edges) after step\nonbreakingspace (3) with $i_t = 3$; eight edges are protected, and the algorithm terminates one step later (no remaining safe pentagonal face in $H_2$). The generating script is \texttt {experiments/draw\_iterated\_reduction\_n14.py}; layouts are Tutte barycentric embeddings with the outer face picked to keep $v_n^{(1)}, v_n^{(2)}$ in the interior.}}{8}{}\protected@file@percent } +\newlabel{fig:iterated-reduction-trace}{{3}{8}} +\newlabel{lem:exactly-one-match}{{3.4}{8}} \newlabel{tocindent-1}{0pt} \newlabel{tocindent0}{0pt} \newlabel{tocindent1}{17.77782pt} \newlabel{tocindent2}{0pt} \newlabel{tocindent3}{0pt} -\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Algorithm\nonbreakingspace 3.1\hbox {} on $G'=\mathrm {dual}(G)$, where $G$ is the first min-degree-$5$ plantri triangulation on $14$ vertices and $\varphi _1$ is a specific proper $3$-edge-colouring of $H_1$ that satisfies both the chord-apex condition (Lemma\nonbreakingspace 2.6\hbox {}) and the Kempe-cycle condition (Lemma\nonbreakingspace 2.7\hbox {}), found by \texttt {experiments/search\_kempe\_property.py}. \emph {Left:} $G'$ ($24$ vertices, $36$ edges) with the chosen pentagonal face shaded. \emph {Centre:} $H_1$ ($20$ vertices, $30$ edges) after step\nonbreakingspace (1) with $i_1 = 1$, $3$-edge-coloured by $\varphi _1$; the four edges around $v_n^{(1)}$ in $E$ are drawn thicker, and the spike and merged edges share the colour green. \emph {Right:} $H_2$ ($16$ vertices, $24$ edges) after step\nonbreakingspace (3) with $i_t = 3$; eight edges are protected, and the algorithm terminates one step later (no remaining safe pentagonal face in $H_2$). The generating script is \texttt {experiments/draw\_iterated\_reduction\_n14.py}; layouts are Tutte barycentric embeddings with the outer face picked to keep $v_n^{(1)}, v_n^{(2)}$ in the interior.}}{8}{}\protected@file@percent } -\newlabel{fig:iterated-reduction-trace}{{3}{8}} -\newlabel{conj:no-all-distinct-coloring}{{3.4}{8}} -\gdef \@abspage@last{8} +\newlabel{lem:all-distinct-exists}{{3.5}{9}} +\newlabel{conj:face-monochromatic-pair-on-merged-kempe-cycle}{{3.6}{9}} +\gdef \@abspage@last{9} diff --git a/papers/dual_decomposition_minimal_counterexamples/paper.fdb_latexmk b/papers/dual_decomposition_minimal_counterexamples/paper.fdb_latexmk index 5e4deec..f3d1005 100644 --- a/papers/dual_decomposition_minimal_counterexamples/paper.fdb_latexmk +++ b/papers/dual_decomposition_minimal_counterexamples/paper.fdb_latexmk @@ -1,6 +1,6 @@ # Fdb version 3 -["pdflatex"] 1779490854 "/Users/didericis/Code/math-research/papers/dual_decomposition_minimal_counterexamples/paper.tex" "paper.pdf" "paper" 1779490855 - "/Users/didericis/Code/math-research/papers/dual_decomposition_minimal_counterexamples/paper.tex" 1779490854 8400 319c3b8b7a4962c7285398f53dc0c37a "" +["pdflatex"] 1779636334 "/Users/didericis/Code/math-research/papers/dual_decomposition_minimal_counterexamples/paper.tex" "paper.pdf" "paper" 1779636335 + "/Users/didericis/Code/math-research/papers/dual_decomposition_minimal_counterexamples/paper.tex" 1779636334 29173 3355ad986dd2045d7c83ee9e1f4197ba "" "/usr/local/texlive/2022/texmf-dist/fonts/map/fontname/texfonts.map" 1577235249 3524 cb3e574dea2d1052e39280babc910dc8 "" "/usr/local/texlive/2022/texmf-dist/fonts/tfm/public/amsfonts/cmextra/cmex7.tfm" 1246382020 1004 54797486969f23fa377b128694d548df "" "/usr/local/texlive/2022/texmf-dist/fonts/tfm/public/amsfonts/cmextra/cmex8.tfm" 1246382020 988 bdf658c3bfc2d96d3c8b02cfc1c94c20 "" @@ -19,17 +19,21 @@ "/usr/local/texlive/2022/texmf-dist/fonts/tfm/public/cm/cmsy6.tfm" 1136768653 1116 933a60c408fc0a863a92debe84b2d294 "" "/usr/local/texlive/2022/texmf-dist/fonts/tfm/public/cm/cmsy8.tfm" 1136768653 1120 8b7d695260f3cff42e636090a8002094 "" "/usr/local/texlive/2022/texmf-dist/fonts/tfm/public/cm/cmti10.tfm" 1136768653 1480 aa8e34af0eb6a2941b776984cf1dfdc4 "" + "/usr/local/texlive/2022/texmf-dist/fonts/tfm/public/cm/cmti7.tfm" 1136768653 1492 86331993fe614793f5e7e755835c31c5 "" "/usr/local/texlive/2022/texmf-dist/fonts/tfm/public/cm/cmti8.tfm" 1136768653 1504 1747189e0441d1c18f3ea56fafc1c480 "" "/usr/local/texlive/2022/texmf-dist/fonts/tfm/public/cm/cmtt10.tfm" 1136768653 768 1321e9409b4137d6fb428ac9dc956269 "" "/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx10.pfb" 1248133631 34811 78b52f49e893bcba91bd7581cdc144c0 "" "/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmcsc10.pfb" 1248133631 32001 6aeea3afe875097b1eb0da29acd61e28 "" "/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmex10.pfb" 1248133631 30251 6afa5cb1d0204815a708a080681d4674 "" "/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb" 1248133631 36299 5f9df58c2139e7edcf37c8fca4bd384d "" + "/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi5.pfb" 1248133631 37912 77d683123f92148345f3fc36a38d9ab1 "" "/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb" 1248133631 36281 c355509802a035cadc5f15869451dcee "" "/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb" 1248133631 35752 024fb6c41858982481f6968b5fc26508 "" + "/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr5.pfb" 1248133631 31809 8670ca339bf94e56da1fc21c80635e2a "" "/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb" 1248133631 32762 224316ccc9ad3ca0423a14971cfa7fc1 "" "/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr8.pfb" 1248133631 32726 0a1aea6fcd6468ee2cf64d891f5c43c8 "" "/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb" 1248133631 32569 5e5ddc8df908dea60932f3c484a54c0d "" + "/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy5.pfb" 1248133631 32915 7bf7720c61a5b3a7ff25b0964421c9b6 "" "/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb" 1248133631 32716 08e384dc442464e7285e891af9f45947 "" "/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb" 1248133631 37944 359e864bd06cde3b1cf57bb20757fb06 "" "/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8.pfb" 1248133631 35660 fb24af7afbadb71801619f1415838111 "" @@ -59,12 +63,18 @@ "/usr/local/texlive/2022/texmf-var/fonts/map/pdftex/updmap/pdftex.map" 1647878959 4410336 7d30a02e9fa9a16d7d1f8d037ba69641 "" "/usr/local/texlive/2022/texmf-var/web2c/pdftex/pdflatex.fmt" 1665017617 2826443 7e98410c533054b636c6470db83a27bc "" "/usr/local/texlive/2022/texmf.cnf" 1647878952 577 209b46be99c9075fd74d4c0369380e8c "" + "fig_alg_step0.png" 1779555533 79063 a44949fedf2f79b9d1af80dda627bad0 "" + "fig_alg_step1.png" 1779555533 81138 4655a02d13b723226d9e88c98f25fc14 "" + "fig_alg_step2.png" 1779555533 78532 6a2ff0be6a6e40110e6632afdb232782 "" + "fig_chord_apex_step1.png" 1779497048 128193 2156b95264c4e7be78a47a8f38e36347 "" + "fig_chord_apex_step2.png" 1779497048 103549 502d6b9497ab67090f34da927b068fdc "" + "fig_chord_apex_step3.png" 1779497048 104380 d3d0e553ec0e4ca7ef3f4de590f42ccb "" "fig_reduced_dual_step1.png" 1779490218 117795 4da7754ac28df9e809cfa1069e081c53 "" "fig_reduced_dual_step2.png" 1779490218 96839 4f94c996220a2758dd0ff21ebdb9b2be "" "fig_reduced_dual_step3.png" 1779490218 102877 d2a5db5532697441e3150e2ad26b9173 "" "fig_reduced_dual_step4.png" 1779490218 107439 b30c7a68e32660f9bd3a8070bdb96944 "" - "paper.aux" 1779490855 1250 5e537a38e8b733147def35d69e964063 "pdflatex" - "paper.tex" 1779490854 8400 319c3b8b7a4962c7285398f53dc0c37a "" + "paper.aux" 1779636335 3620 34f7ba6436aaccd7664676641a126dbe "pdflatex" + "paper.tex" 1779636334 29173 3355ad986dd2045d7c83ee9e1f4197ba "" (generated) "paper.aux" "paper.log" diff --git a/papers/dual_decomposition_minimal_counterexamples/paper.fls b/papers/dual_decomposition_minimal_counterexamples/paper.fls index 95cc53a..1cea369 100644 --- a/papers/dual_decomposition_minimal_counterexamples/paper.fls +++ b/papers/dual_decomposition_minimal_counterexamples/paper.fls @@ -247,17 +247,52 @@ INPUT ./fig_reduced_dual_step4.png INPUT fig_reduced_dual_step4.png INPUT ./fig_reduced_dual_step4.png INPUT ./fig_reduced_dual_step4.png +INPUT /usr/local/texlive/2022/texmf-dist/fonts/tfm/public/cm/cmti7.tfm +INPUT /usr/local/texlive/2022/texmf-dist/fonts/tfm/public/cm/cmti7.tfm +INPUT ./fig_chord_apex_step1.png +INPUT ./fig_chord_apex_step1.png +INPUT fig_chord_apex_step1.png +INPUT ./fig_chord_apex_step1.png +INPUT ./fig_chord_apex_step1.png +INPUT ./fig_chord_apex_step2.png +INPUT ./fig_chord_apex_step2.png +INPUT fig_chord_apex_step2.png +INPUT ./fig_chord_apex_step2.png +INPUT ./fig_chord_apex_step2.png +INPUT ./fig_chord_apex_step3.png +INPUT ./fig_chord_apex_step3.png +INPUT fig_chord_apex_step3.png +INPUT ./fig_chord_apex_step3.png +INPUT ./fig_chord_apex_step3.png +INPUT ./fig_alg_step0.png +INPUT ./fig_alg_step0.png +INPUT fig_alg_step0.png +INPUT ./fig_alg_step0.png +INPUT ./fig_alg_step0.png +INPUT ./fig_alg_step1.png +INPUT ./fig_alg_step1.png +INPUT fig_alg_step1.png +INPUT ./fig_alg_step1.png +INPUT ./fig_alg_step1.png +INPUT ./fig_alg_step2.png +INPUT ./fig_alg_step2.png +INPUT fig_alg_step2.png +INPUT ./fig_alg_step2.png +INPUT ./fig_alg_step2.png INPUT /usr/local/texlive/2022/texmf-dist/fonts/tfm/public/cm/cmtt10.tfm INPUT paper.aux INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx10.pfb INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmcsc10.pfb INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmex10.pfb INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb +INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi5.pfb INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb +INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr5.pfb INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr8.pfb INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb +INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy5.pfb INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8.pfb diff --git a/papers/dual_decomposition_minimal_counterexamples/paper.log b/papers/dual_decomposition_minimal_counterexamples/paper.log index 3d46aed..ebc5fd5 100644 --- a/papers/dual_decomposition_minimal_counterexamples/paper.log +++ b/papers/dual_decomposition_minimal_counterexamples/paper.log @@ -1,12 +1,12 @@ -This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022) (preloaded format=pdflatex 2022.10.5) 23 MAY 2026 13:19 +This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022) (preloaded format=pdflatex 2022.10.5) 24 MAY 2026 11:25 entering extended mode restricted \write18 enabled. + file:line:error style messages enabled. %&-line parsing enabled. -**paper.tex -(./paper.tex +**/Users/didericis/Code/math-research/papers/dual_decomposition_minimal_counterexamples/paper.tex +(/Users/didericis/Code/math-research/papers/dual_decomposition_minimal_counterexamples/paper.tex LaTeX2e <2021-11-15> patch level 1 -L3 programming layer <2022-02-24> -(/usr/local/texlive/2022/texmf-dist/tex/latex/amscls/amsart.cls +L3 programming layer <2022-02-24> (/usr/local/texlive/2022/texmf-dist/tex/latex/amscls/amsart.cls Document Class: amsart 2020/05/29 v2.20.6 \linespacing=\dimen138 \normalparindent=\dimen139 @@ -18,17 +18,14 @@ Package: amsmath 2021/10/15 v2.17l AMS math features For additional information on amsmath, use the `?' option. (/usr/local/texlive/2022/texmf-dist/tex/latex/amsmath/amstext.sty Package: amstext 2021/08/26 v2.01 AMS text - -(/usr/local/texlive/2022/texmf-dist/tex/latex/amsmath/amsgen.sty + (/usr/local/texlive/2022/texmf-dist/tex/latex/amsmath/amsgen.sty File: amsgen.sty 1999/11/30 v2.0 generic functions \@emptytoks=\toks16 \ex@=\dimen140 -)) -(/usr/local/texlive/2022/texmf-dist/tex/latex/amsmath/amsbsy.sty +)) (/usr/local/texlive/2022/texmf-dist/tex/latex/amsmath/amsbsy.sty Package: amsbsy 1999/11/29 v1.2d Bold Symbols \pmbraise@=\dimen141 -) -(/usr/local/texlive/2022/texmf-dist/tex/latex/amsmath/amsopn.sty +) (/usr/local/texlive/2022/texmf-dist/tex/latex/amsmath/amsopn.sty Package: amsopn 2021/08/26 v2.02 operator names ) \inf@bad=\count185 @@ -69,13 +66,10 @@ LaTeX Font Info: Redeclaring font encoding OMS on input line 744. LaTeX Info: Redefining \[ on input line 2938. LaTeX Info: Redefining \] on input line 2939. ) -LaTeX Font Info: Trying to load font information for U+msa on input line 397 -. - -(/usr/local/texlive/2022/texmf-dist/tex/latex/amsfonts/umsa.fd +LaTeX Font Info: Trying to load font information for U+msa on input line 397. + (/usr/local/texlive/2022/texmf-dist/tex/latex/amsfonts/umsa.fd File: umsa.fd 2013/01/14 v3.01 AMS symbols A -) -(/usr/local/texlive/2022/texmf-dist/tex/latex/amsfonts/amsfonts.sty +) (/usr/local/texlive/2022/texmf-dist/tex/latex/amsfonts/amsfonts.sty Package: amsfonts 2013/01/14 v3.01 Basic AMSFonts support \symAMSa=\mathgroup4 \symAMSb=\mathgroup5 @@ -106,42 +100,33 @@ LaTeX Font Info: Overwriting math alphabet `\mathfrak' in version `bold' \thm@postskip=\skip55 \thm@headsep=\skip56 \dth@everypar=\toks26 -) -(/usr/local/texlive/2022/texmf-dist/tex/latex/amsfonts/amssymb.sty +) (/usr/local/texlive/2022/texmf-dist/tex/latex/amsfonts/amssymb.sty Package: amssymb 2013/01/14 v3.01 AMS font symbols -) -(/usr/local/texlive/2022/texmf-dist/tex/latex/graphics/graphicx.sty +) (/usr/local/texlive/2022/texmf-dist/tex/latex/graphics/graphicx.sty Package: graphicx 2021/09/16 v1.2d Enhanced LaTeX Graphics (DPC,SPQR) - -(/usr/local/texlive/2022/texmf-dist/tex/latex/graphics/keyval.sty + (/usr/local/texlive/2022/texmf-dist/tex/latex/graphics/keyval.sty Package: keyval 2014/10/28 v1.15 key=value parser (DPC) \KV@toks@=\toks27 -) -(/usr/local/texlive/2022/texmf-dist/tex/latex/graphics/graphics.sty +) (/usr/local/texlive/2022/texmf-dist/tex/latex/graphics/graphics.sty Package: graphics 2021/03/04 v1.4d Standard LaTeX Graphics (DPC,SPQR) - -(/usr/local/texlive/2022/texmf-dist/tex/latex/graphics/trig.sty + (/usr/local/texlive/2022/texmf-dist/tex/latex/graphics/trig.sty Package: trig 2021/08/11 v1.11 sin cos tan (DPC) -) -(/usr/local/texlive/2022/texmf-dist/tex/latex/graphics-cfg/graphics.cfg +) (/usr/local/texlive/2022/texmf-dist/tex/latex/graphics-cfg/graphics.cfg File: graphics.cfg 2016/06/04 v1.11 sample graphics configuration ) Package graphics Info: Driver file: pdftex.def on input line 107. - -(/usr/local/texlive/2022/texmf-dist/tex/latex/graphics-def/pdftex.def + (/usr/local/texlive/2022/texmf-dist/tex/latex/graphics-def/pdftex.def File: pdftex.def 2020/10/05 v1.2a Graphics/color driver for pdftex )) \Gin@req@height=\dimen150 \Gin@req@width=\dimen151 ) \c@theorem=\count272 - -(/usr/local/texlive/2022/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def + (/usr/local/texlive/2022/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def File: l3backend-pdftex.def 2022-02-07 L3 backend support: PDF output (pdfTeX) \l__color_backend_stack_int=\count273 \l__pdf_internal_box=\box53 -) -(./paper.aux) +) (./paper.aux) \openout1 = `paper.aux'. LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 27. @@ -159,17 +144,13 @@ LaTeX Font Info: ... okay on input line 27. LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 27. LaTeX Font Info: ... okay on input line 27. LaTeX Font Info: Trying to load font information for U+msa on input line 27. - (/usr/local/texlive/2022/texmf-dist/tex/latex/amsfonts/umsa.fd File: umsa.fd 2013/01/14 v3.01 AMS symbols A ) LaTeX Font Info: Trying to load font information for U+msb on input line 27. - - -(/usr/local/texlive/2022/texmf-dist/tex/latex/amsfonts/umsb.fd + (/usr/local/texlive/2022/texmf-dist/tex/latex/amsfonts/umsb.fd File: umsb.fd 2013/01/14 v3.01 AMS symbols B -) -(/usr/local/texlive/2022/texmf-dist/tex/context/base/mkii/supp-pdf.mkii +) (/usr/local/texlive/2022/texmf-dist/tex/context/base/mkii/supp-pdf.mkii [Loading MPS to PDF converter (version 2006.09.02).] \scratchcounter=\count274 \scratchdimen=\dimen152 @@ -184,18 +165,12 @@ File: umsb.fd 2013/01/14 v3.01 AMS symbols B \everyMPtoPDFconversion=\toks29 ) (/usr/local/texlive/2022/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty Package: epstopdf-base 2020-01-24 v2.11 Base part for package epstopdf -Package epstopdf-base Info: Redefining graphics rule for `.eps' on input line 4 -85. - -(/usr/local/texlive/2022/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg -File: epstopdf-sys.cfg 2010/07/13 v1.3 Configuration of (r)epstopdf for TeX Liv -e -)) -[1{/usr/local/texlive/2022/texmf-var/fonts/map/pdftex/updmap/pdftex.map}] +Package epstopdf-base Info: Redefining graphics rule for `.eps' on input line 485. + (/usr/local/texlive/2022/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg +File: epstopdf-sys.cfg 2010/07/13 v1.3 Configuration of (r)epstopdf for TeX Live +)) [1{/usr/local/texlive/2022/texmf-var/fonts/map/pdftex/updmap/pdftex.map}] Overfull \hbox (41.917pt too wide) in paragraph at lines 145--147 -[]\OT1/cmr/m/n/10 List the five degree-$2$ ver-tices in clock-wise or-der aroun -d $\OML/cmm/m/it/10 F$ \OT1/cmr/m/n/10 as $\OML/cmm/m/it/10 A \OT1/cmr/m/n/10 = - (\OML/cmm/m/it/10 A[]; A[]; A[]; A[]; A[]\OT1/cmr/m/n/10 )$. +[]\OT1/cmr/m/n/10 List the five degree-$2$ ver-tices in clock-wise or-der around $\OML/cmm/m/it/10 F$ \OT1/cmr/m/n/10 as $\OML/cmm/m/it/10 A \OT1/cmr/m/n/10 = (\OML/cmm/m/it/10 A[]; A[]; A[]; A[]; A[]\OT1/cmr/m/n/10 )$. [] @@ -221,8 +196,7 @@ Package pdftex.def Info: fig_reduced_dual_step4.png used on input line 168. LaTeX Warning: `h' float specifier changed to `ht'. -[2] [3 <./fig_reduced_dual_step1.png> <./fig_reduced_dual_step2.png> <./fig_red -uced_dual_step3.png> <./fig_reduced_dual_step4.png>] +[2] [3 <./fig_reduced_dual_step1.png> <./fig_reduced_dual_step2.png> <./fig_reduced_dual_step3.png> <./fig_reduced_dual_step4.png>] File: fig_chord_apex_step1.png Graphic file (type png) @@ -242,15 +216,9 @@ Package pdftex.def Info: fig_chord_apex_step3.png used on input line 291. LaTeX Warning: `h' float specifier changed to `ht'. -[4] [5 <./fig_chord_apex_step1.png> <./fig_chord_apex_step2.png> <./fig_chord_a -pex_step3.png>] [6] +[4] [5 <./fig_chord_apex_step1.png> <./fig_chord_apex_step2.png> <./fig_chord_apex_step3.png>] [6] Overfull \hbox (4.76643pt too wide) in paragraph at lines 433--440 -\OT1/cmr/m/n/10 which $\OML/cmm/m/it/10 '[]\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 f[ -]\OT1/cmr/m/n/10 ) = \OML/cmm/m/it/10 '[]\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 f[]\ -OT1/cmr/m/n/10 )$ and $\OML/cmm/m/it/10 '[]\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 f[ -]\OT1/cmr/m/n/10 )\OML/cmm/m/it/10 ; '[]\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 f[]\O -T1/cmr/m/n/10 )\OML/cmm/m/it/10 ; '[]\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 f[]\OT1/ -cmr/m/n/10 )$ +\OT1/cmr/m/n/10 which $\OML/cmm/m/it/10 '[]\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 f[]\OT1/cmr/m/n/10 ) = \OML/cmm/m/it/10 '[]\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 f[]\OT1/cmr/m/n/10 )$ and $\OML/cmm/m/it/10 '[]\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 f[]\OT1/cmr/m/n/10 )\OML/cmm/m/it/10 ; '[]\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 f[]\OT1/cmr/m/n/10 )\OML/cmm/m/it/10 ; '[]\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 f[]\OT1/cmr/m/n/10 )$ [] @@ -270,21 +238,17 @@ Package pdftex.def Info: fig_alg_step2.png used on input line 481. (pdftex.def) Requested size: 115.20264pt x 132.48134pt. Underfull \hbox (badness 4391) in paragraph at lines 498--498 -\OT1/cmr/m/sc/10 Figure 3.\OT1/cmr/m/n/10 Algorithm 3.1[] on $\OML/cmm/m/it/10 -G[] \OT1/cmr/m/n/10 = [](\OML/cmm/m/it/10 G\OT1/cmr/m/n/10 )$, where $\OML/cmm/ -m/it/10 G$ +\OT1/cmr/m/sc/10 Figure 3.\OT1/cmr/m/n/10 Algorithm 3.1[] on $\OML/cmm/m/it/10 G[] \OT1/cmr/m/n/10 = [](\OML/cmm/m/it/10 G\OT1/cmr/m/n/10 )$, where $\OML/cmm/m/it/10 G$ [] Underfull \hbox (badness 3623) in paragraph at lines 498--498 -\OT1/cmr/m/n/10 is the first min-degree-$5$ plantri tri-an-gu-la-tion on $14$ v -er- +\OT1/cmr/m/n/10 is the first min-degree-$5$ plantri tri-an-gu-la-tion on $14$ ver- [] Underfull \hbox (badness 3179) in paragraph at lines 498--498 -\OT1/cmr/m/n/10 tices and $\OML/cmm/m/it/10 '[]$ \OT1/cmr/m/n/10 is a spe-cific - proper $3$-edge-colouring of $\OML/cmm/m/it/10 H[]$ +\OT1/cmr/m/n/10 tices and $\OML/cmm/m/it/10 '[]$ \OT1/cmr/m/n/10 is a spe-cific proper $3$-edge-colouring of $\OML/cmm/m/it/10 H[]$ [] @@ -297,37 +261,20 @@ Underfull \hbox (badness 6094) in paragraph at lines 498--498 \OT1/cmr/m/n/10 and the Kempe-cycle con-di-tion (Lemma 2.7[]), found by [] -[7] [8 <./fig_alg_step0.png> <./fig_alg_step1.png> <./fig_alg_step2.png>] -(./paper.aux) ) +[7] [8 <./fig_alg_step0.png> <./fig_alg_step1.png> <./fig_alg_step2.png>] [9] (./paper.aux) ) Here is how much of TeX's memory you used: - 3079 strings out of 478268 - 43848 string characters out of 5846347 - 344259 words of memory out of 5000000 - 21116 multiletter control sequences out of 15000+600000 + 3082 strings out of 478268 + 44173 string characters out of 5846347 + 344279 words of memory out of 5000000 + 21118 multiletter control sequences out of 15000+600000 476532 words of font info for 56 fonts, out of 8000000 for 9000 1302 hyphenation exceptions out of 8191 - 69i,8n,76p,1306b,298s stack positions out of 10000i,1000n,20000p,200000b,200000s - - -Output written on paper.pdf (8 pages, 969703 bytes). + 69i,8n,76p,1392b,298s stack positions out of 10000i,1000n,20000p,200000b,200000s + +Output written on paper.pdf (9 pages, 977618 bytes). PDF statistics: - 137 PDF objects out of 1000 (max. 8388607) - 72 compressed objects within 1 object stream + 140 PDF objects out of 1000 (max. 8388607) + 74 compressed objects within 1 object stream 0 named destinations out of 1000 (max. 500000) 51 words of extra memory for PDF output out of 10000 (max. 10000000) diff --git a/papers/dual_decomposition_minimal_counterexamples/paper.pdf b/papers/dual_decomposition_minimal_counterexamples/paper.pdf index bb72059..a4f46b4 100644 Binary files a/papers/dual_decomposition_minimal_counterexamples/paper.pdf and b/papers/dual_decomposition_minimal_counterexamples/paper.pdf differ diff --git a/papers/dual_decomposition_minimal_counterexamples/paper.tex b/papers/dual_decomposition_minimal_counterexamples/paper.tex index 3a2326c..936e5af 100644 --- a/papers/dual_decomposition_minimal_counterexamples/paper.tex +++ b/papers/dual_decomposition_minimal_counterexamples/paper.tex @@ -499,16 +499,121 @@ v_n^{(2)}$ in the interior.} \label{fig:iterated-reduction-trace} \end{figure} +\begin{lemma}[Exactly one matching pair in the algorithm's output] +\label{lem:exactly-one-match} +Let $G$ be a minimal counterexample to the Four Colour Theorem, and let +$(H_{t^*}, \varphi_{t^*})$ be the final graph-and-colouring produced by some +terminating execution of Algorithm~\ref{alg:iterated-reduction} on $G$, with +named pairs $(\mathrm{spike}_t, \mathrm{merged}_t)$ for $t = 1, \dots, t^*$. +Then there is exactly one $t$ with +$\varphi_{t^*}(\mathrm{spike}_t) = \varphi_{t^*}(\mathrm{merged}_t)$, and it +is $t = 1$. +\end{lemma} + +\begin{proof} +The algorithm never re-colours an existing edge: at each iteration +step~(3d) every surviving edge keeps its $\varphi_{t-1}$-colour, and the +four new edges receive fresh colours forced by propriety. Hence for every +$1 \leq k \leq t \leq t^*$, +\[ + \varphi_t(\mathrm{spike}_k) = \varphi_k(\mathrm{spike}_k), + \qquad + \varphi_t(\mathrm{merged}_k) = \varphi_k(\mathrm{merged}_k); +\] +the colours of the step-$k$ named edges, once written, are permanent. It +suffices to compare $\varphi_k(\mathrm{spike}_k)$ and +$\varphi_k(\mathrm{merged}_k)$ at the step where each pair is introduced. + +\textbf{Case $k = 1$.} Since $G$ is a minimal counterexample, $H_1$ is a +reduced dual of $G'$. Lemma~\ref{lem:chord-apex} applied to $\varphi_1$ gives +$\varphi_1(\mathrm{spike}_1) = \varphi_1(\mathrm{merged}_1)$. + +\textbf{Case $k \geq 2$.} At step $k$ the algorithm picks an index $i_k$ for +which $f_{i_k+3} = f_{i_k+4}$ (chord consistency) and $f_{i_k}, f_{i_k+1}, +f_{i_k+2}$ are pairwise distinct (propriety at the new $v_n$), where $f$ is +the external vector of the chosen pentagonal face of $H_{k-1}$ under +$\varphi_{k-1}$. Step~(3d) then assigns +\[ + \varphi_k(\mathrm{spike}_k) = f_{i_k+1}, + \qquad + \varphi_k(\mathrm{merged}_k) = f_{i_k+3}. +\] +By Lemma~\ref{lem:pentagonal-externals}, $f$ has the $(2,2,1)$ pattern: a +block of three consecutive positions $\{p, p+1, p+2\}$ (mod $5$) on which it +is constantly some colour $c$, while the remaining two positions +$\{p+3, p+4\}$ hold the two non-$c$ colours, one each. The condition +$f_{i_k+3} = f_{i_k+4}$ forces $(i_k+3, i_k+4)$ to be either $(p, p+1)$ or +$(p+1, p+2)$ --- the two consecutive pairs inside the block --- and +correspondingly $i_k + 1 \in \{p+3, p+4\}$, \emph{outside} the block. So +$f_{i_k+1}$ is not $c$, whereas $f_{i_k+3} = c$, and hence +$\varphi_k(\mathrm{spike}_k) \neq \varphi_k(\mathrm{merged}_k)$. + +Combining the two cases, exactly one $t \in \{1, \dots, t^*\}$ --- namely +$t = 1$ --- has $\varphi_{t^*}(\mathrm{spike}_t) = +\varphi_{t^*}(\mathrm{merged}_t)$. +\end{proof} + +\begin{lemma}[All-distinct colouring exists on a 4-colourable graph] +\label{lem:all-distinct-exists} +Let $G$ be a $4$-colourable maximal planar graph of minimum degree $\geq 5$ +(equivalently, a maximal planar graph that is \emph{not} a minimal +counterexample to the Four Colour Theorem). Then there is an execution of +Algorithm~\ref{alg:iterated-reduction} on $G$ whose final colouring +$\varphi_{t^*}$ satisfies +$\varphi_{t^*}(\mathrm{spike}_t) \neq \varphi_{t^*}(\mathrm{merged}_t)$ for +every $t \in \{1, \dots, t^*\}$. In particular, there exists a proper +$3$-edge-colouring of $H_{t^*}$ under which every spike-merged pair has +distinct colours. +\end{lemma} + +\begin{proof} +The argument mirrors Lemma~\ref{lem:exactly-one-match}, but extends a +colouring \emph{downward} from $G'$ rather than carrying one forward from +$H_1$. + +Since $G$ is $4$-colourable, by Tait's theorem +$G' = \mathrm{dual}(G)$ admits a proper $3$-edge-colouring $\xi$. Apply +Lemma~\ref{lem:pentagonal-externals} to $\xi$ at the pentagonal face $F_v$ +selected in step~(1): the external vector $f = (f_0, \dots, f_4)$ at $F_v$ +under $\xi$ has the $(3,1,1)$ cyclic-consecutive shape, with a block of +three consecutive positions $\{p, p+1, p+2\}$ (mod $5$) holding a common +colour $c$, and the remaining two positions $\{p+3, p+4\}$ holding the two +non-$c$ colours, one each. The algorithm's choice of $i_1$ forces +$\{i_1+3, i_1+4\}$ inside the $c$-block (so the chord is consistently +coloured) and the three positions $\{i_1, i_1+1, i_1+2\}$ pairwise distinct; +in particular $i_1+1$ lies \emph{outside} the $c$-block. + +Choose $\varphi_1$ to be the proper $3$-edge-colouring of $H_1$ that agrees +with $\xi$ on every surviving edge and assigns each new edge at $A_j$ the +unique third colour at $A_j$. Then +$\varphi_1(\mathrm{spike}_1) = f_{i_1+1}$, a value not equal to $c$, while +$\varphi_1(\mathrm{merged}_1) = f_{i_1+3} = c$, so +$\varphi_1(\mathrm{spike}_1) \neq \varphi_1(\mathrm{merged}_1)$. + +The same argument repeats at every step $k \geq 2$: the external vector at +the chosen pentagonal face under $\varphi_{k-1}$ has the $(3,1,1)$ +cyclic-consecutive shape (Lemma~\ref{lem:pentagonal-externals}), the +algorithm's index choice $i_k$ puts $i_k+3, i_k+4$ inside the colour block +and $i_k+1$ outside, and step~(3d) thus assigns +$\varphi_k(\mathrm{spike}_k) \neq \varphi_k(\mathrm{merged}_k)$. The +algorithm preserves these colours through every later step, so +$\varphi_{t^*}(\mathrm{spike}_t) \neq \varphi_{t^*}(\mathrm{merged}_t)$ for +every $t \in \{1, \dots, t^*\}$. +\end{proof} + \begin{conjecture} -\label{conj:no-all-distinct-coloring} -Let $G$ be a maximal planar graph of minimum degree $\geq 5$, and let -$H_{t^*}$ be the final reduced graph produced by some terminating execution -of Algorithm~\ref{alg:iterated-reduction} on $G$, with the corresponding -sequence of named pairs $(\mathrm{spike}_t, \mathrm{merged}_t)$ for -$t = 1, \dots, t^*$. Then $G$ is a minimal counterexample to the Four Colour -Theorem if and only if there is no proper $3$-edge-colouring of $H_{t^*}$ -under which $\mathrm{spike}_t$ and $\mathrm{merged}_t$ receive different -colours for every $t \in \{1, \dots, t^*\}$. +\label{conj:face-monochromatic-pair-on-merged-kempe-cycle} +Let $G$ be a minimal counterexample to the Four Colour Theorem, and let +$\widehat{G}'_{v,i}$ be a reduced dual of $G' = \mathrm{dual}(G)$. Then for +every proper $3$-edge-colouring $\varphi$ of $\widehat{G}'_{v,i}$ there exist +a face $F$ of $\widehat{G}'_{v,i}$ and two distinct edges +$e_1, e_2 \in \partial F$, with neither $e_1$ nor $e_2$ equal to the merged +edge, such that +\begin{enumerate} + \item $\varphi(e_1) = \varphi(e_2)$, and + \item $e_1$, $e_2$, and the merged edge all lie on a common + $\{a, b\}$-Kempe cycle of $\varphi$. +\end{enumerate} \end{conjecture} \end{document}