diff --git a/papers/dual_decomposition_minimal_counterexamples/experiments/check_dodecahedron_kempe.py b/papers/dual_decomposition_minimal_counterexamples/experiments/check_dodecahedron_kempe.py new file mode 100644 index 0000000..c6a2534 --- /dev/null +++ b/papers/dual_decomposition_minimal_counterexamples/experiments/check_dodecahedron_kempe.py @@ -0,0 +1,186 @@ +"""Check whether the dodecahedron's reduced dual admits a proper +3-edge-colouring with: + (i) colour(spike) == colour(merged), AND + (ii) the {c_spike, c_side0}-Kempe cycle through the spike contains both + side-0 and the merged edge, AND + (iii) the {c_spike, c_side1}-Kempe cycle through the spike contains both + side-1 and the merged edge. + +Definitions follow Algorithm 3.1 in paper.tex with G = icosahedron, G' = +dodecahedron, i_1 = 0; the reduced dual has 16 vertices and 24 edges. + +Lemmas 2.6 and 2.7 force these properties for ANY proper 3-edge-colouring +of the reduced dual of a *minimal counterexample's* dual. The dodecahedron +is the dual of the icosahedron --- which IS 4-colourable, so the lemmas do +not apply and the question is non-trivial. +""" +from sage.all import Graph + + +def build_reduced_dodecahedron(i_red=0): + 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))) + v_n = 'v_n' + edges.append((v_n, ('b', i_red % 5))) + edges.append((v_n, ('b', (i_red + 1) % 5))) + edges.append((v_n, ('b', (i_red + 2) % 5))) + edges.append((('b', (i_red + 3) % 5), ('b', (i_red + 4) % 5))) + return Graph(edges, multiedges=False, loops=False) + + +def enumerate_proper_3_edge_colorings(G): + """Return (edge_list, list_of_colorings) where each coloring is a list of + 3-edge-colours indexed by edge_list.""" + 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(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, coloring, start_edge_idx, color_pair): + """Return the set of edge-indices in the Kempe cycle containing + edges[start_edge_idx] in the subgraph of edges with colour in + color_pair.""" + a, b = color_pair + in_sub = [i for i in range(len(edges)) if coloring[i] in (a, b)] + if start_edge_idx not in in_sub: + return None + visited = {start_edge_idx} + stack = [start_edge_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 main(): + G = build_reduced_dodecahedron(i_red=0) + print(f"|V| = {G.order()}, |E| = {G.size()}") + + edges, colorings = enumerate_proper_3_edge_colorings(G) + print(f"Proper 3-edge-colorings total: {len(colorings)}") + + v_n = 'v_n' + spike_set = frozenset({v_n, ('b', 1)}) + side_0_set = frozenset({v_n, ('b', 0)}) + side_1_set = frozenset({v_n, ('b', 2)}) + merged_set = frozenset({('b', 3), ('b', 4)}) + + idx = {} + for i, e in enumerate(edges): + s = frozenset((e[0], e[1])) + if s == spike_set: idx['spike'] = i + if s == side_0_set: idx['side_0'] = i + if s == side_1_set: idx['side_1'] = i + if s == merged_set: idx['merged'] = i + + n_chord_apex = 0 # spike == merged + n_kc0_ok = 0 # condition (ii) + n_kc1_ok = 0 # condition (iii) + n_all_ok = 0 # all three + example = None + + for col in colorings: + c_spike = col[idx['spike']] + c_merged = col[idx['merged']] + c_s0 = col[idx['side_0']] + c_s1 = col[idx['side_1']] + if c_spike != c_merged: + continue + n_chord_apex += 1 + + kc0 = kempe_cycle_edges(edges, col, idx['spike'], (c_spike, c_s0)) + kc1 = kempe_cycle_edges(edges, col, idx['spike'], (c_spike, c_s1)) + + kc0_ok = kc0 is not None and idx['side_0'] in kc0 and idx['merged'] in kc0 + kc1_ok = kc1 is not None and idx['side_1'] in kc1 and idx['merged'] in kc1 + n_kc0_ok += int(kc0_ok) + n_kc1_ok += int(kc1_ok) + if kc0_ok and kc1_ok: + n_all_ok += 1 + if example is None: + example = (col, kc0, kc1) + + print() + print(f"Colorings with spike == merged (chord-apex condition): {n_chord_apex}") + print(f" ... + {{c, c_0}}-Kempe cycle through spike/side-0/merged: {n_kc0_ok}") + print(f" ... + {{c, c_1}}-Kempe cycle through spike/side-1/merged: {n_kc1_ok}") + print(f" ... ALL THREE conditions: {n_all_ok}") + + if example is not None: + col, kc0, kc1 = example + c_spike = col[idx['spike']] + print() + print("Example coloring (one of {} matching):".format(n_all_ok)) + for role in ('spike', 'side_0', 'side_1', 'merged'): + print(f" {role:7s}: colour {col[idx[role]]}, edge {tuple(edges[idx[role]])}") + print(f" spike colour = merged colour = {c_spike}") + print(f" Kempe cycle {{c, c_0}} (through spike): {len(kc0)} edges") + for i in sorted(kc0): + print(f" [c={col[i]}] {edges[i]}") + print(f" Kempe cycle {{c, c_1}} (through spike): {len(kc1)} edges") + for i in sorted(kc1): + print(f" [c={col[i]}] {edges[i]}") + else: + # Dissect a sample chord-apex coloring that fails the Kempe condition + print() + print("Sample chord-apex coloring (fails the Kempe-chain condition):") + for col in colorings: + if col[idx['spike']] != col[idx['merged']]: + continue + c_spike = col[idx['spike']] + c_s0 = col[idx['side_0']] + c_s1 = col[idx['side_1']] + for role in ('spike', 'side_0', 'side_1', 'merged'): + print(f" {role:7s}: colour {col[idx[role]]}, edge {tuple(edges[idx[role]])}") + kc0 = kempe_cycle_edges(edges, col, idx['spike'], (c_spike, c_s0)) + kc1 = kempe_cycle_edges(edges, col, idx['spike'], (c_spike, c_s1)) + kc_m0 = kempe_cycle_edges(edges, col, idx['merged'], (c_spike, c_s0)) + kc_m1 = kempe_cycle_edges(edges, col, idx['merged'], (c_spike, c_s1)) + print(f" spike's {{c, c_0}}-Kempe cycle has {len(kc0)} edges; " + f"side_0 in it = {idx['side_0'] in kc0}, " + f"merged in it = {idx['merged'] in kc0}") + print(f" merged's {{c, c_0}}-Kempe cycle has {len(kc_m0)} edges; " + f"disjoint from spike's? {kc0.isdisjoint(kc_m0)}") + print(f" spike's {{c, c_1}}-Kempe cycle has {len(kc1)} edges; " + f"side_1 in it = {idx['side_1'] in kc1}, " + f"merged in it = {idx['merged'] in kc1}") + print(f" merged's {{c, c_1}}-Kempe cycle has {len(kc_m1)} edges; " + f"disjoint from spike's? {kc1.isdisjoint(kc_m1)}") + break + + +if __name__ == '__main__': + main() diff --git a/papers/dual_decomposition_minimal_counterexamples/experiments/draw_iterated_reduction.py b/papers/dual_decomposition_minimal_counterexamples/experiments/draw_iterated_reduction.py new file mode 100644 index 0000000..2e8d522 --- /dev/null +++ b/papers/dual_decomposition_minimal_counterexamples/experiments/draw_iterated_reduction.py @@ -0,0 +1,219 @@ +"""Draw the iterated reduction algorithm's trace on the dodecahedron. + +Produces three figures: + fig_alg_step0.png -- G' (dodecahedron) with F_v (inner pentagon) shaded. + fig_alg_step1.png -- H_1 (post step 1), 3-edge-coloured; 4 protected edges. + fig_alg_step2.png -- H_2 (post step 2), 3-edge-coloured; 8 protected edges; + algorithm terminates. + +Run with: sage experiments/draw_iterated_reduction.py +""" +from sage.all import Graph +from sage.graphs.graph_coloring import edge_coloring +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'] # proper-edge-colour palette +GRAY = '#9ca3af' +DARK = '#374151' +HIGHLIGHT = '#fef3c7' + + +def dodecahedron_positions(): + pos = {} + R = {'a': 1.0, 'b': 2.2, 'c': 3.6, 'd': 4.8} + for i in range(5): + for fam in ('a', 'b'): + th = math.radians(90 - 72 * i) + pos[(fam, i)] = (R[fam] * math.cos(th), R[fam] * math.sin(th)) + for fam in ('c', 'd'): + th = math.radians(90 - 72 * i - 36) + pos[(fam, i)] = (R[fam] * math.cos(th), R[fam] * math.sin(th)) + return pos + + +def build_dodecahedron(): + edges = [] + for i in range(5): + edges.append((('a', i), ('a', (i + 1) % 5))) + edges.append((('a', i), ('b', i))) + edges.append((('b', i), ('c', i))) + edges.append((('b', i), ('c', (i - 1) % 5))) + edges.append((('c', i), ('d', i))) + edges.append((('d', i), ('d', (i + 1) % 5))) + G = Graph(edges, multiedges=False, loops=False) + G.is_planar(set_embedding=True) + return G + + +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 = [] + for B_k in boundary: + outer = [w for w in G.neighbor_iterator(B_k) if w not in boundary] + if len(outer) != 1: + break + externals.append(frozenset([B_k, outer[0]])) + A.append(outer[0]) + else: + if not any(e in protected for e in boundary_edges + externals): + return boundary, externals, A + return None + + +def valid_indices(f_vec): + out = [] + 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: + out.append(i) + return out + + +def draw(ax, G, pos, *, coloring=None, protected=None, + shade_face=None): + if shade_face: + poly = [pos[v] for v in shade_face] + ax.add_patch(Polygon(poly, closed=True, facecolor=HIGHLIGHT, + edgecolor='none', zorder=0)) + protected = protected or set() + for u, v in G.edges(labels=False): + e = frozenset([u, v]) + c = C[coloring[e]] if coloring is not None else GRAY + lw = 3.8 if e in 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 G.vertices(sort=False): + x, y = pos[v] + if isinstance(v, tuple) and v[0] == 'v_n': + t = v[1] + ax.scatter(x, y, s=320, color=HIGHLIGHT, marker='s', + edgecolors='black', linewidths=1.2, zorder=4) + ax.annotate(f'$v_n^{{({t})}}$', (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) + ax.set_aspect('equal') + ax.axis('off') + + +def main(): + G = build_dodecahedron() + pos = dodecahedron_positions() + F_v = [('a', i) for i in range(5)] + + # ----- Step 0: G' with F_v shaded ----- + fig, ax = plt.subplots(figsize=(8, 8)) + draw(ax, G, pos, shade_face=F_v) + fig.savefig(os.path.join(OUT_DIR, 'fig_alg_step0.png'), + dpi=170, bbox_inches='tight') + plt.close(fig) + + # ----- Step 1: Definition 2.1 at F_v with i_1 = 0 ----- + safe = find_safe_pentagonal_face(G, set()) + boundary_1, externals_1, A_1 = safe + G1 = G.copy() + for v in boundary_1: + G1.delete_vertex(v) + v_n_1 = ('v_n', 1) + G1.add_vertex(v_n_1) + G1.add_edge(v_n_1, A_1[0]) + G1.add_edge(v_n_1, A_1[1]) + G1.add_edge(v_n_1, A_1[2]) + G1.add_edge(A_1[3], A_1[4]) + G1.is_planar(set_embedding=True) + pos1 = {v: p for v, p in pos.items() if v not in boundary_1} + cx = (pos[A_1[0]][0] + pos[A_1[1]][0] + pos[A_1[2]][0]) / 3 + cy = (pos[A_1[0]][1] + pos[A_1[1]][1] + pos[A_1[2]][1]) / 3 + pos1[v_n_1] = (cx * 0.55, cy * 0.55) + + cols = edge_coloring(G1, value_only=False) + coloring = {} + for k, edge_list in enumerate(cols): + for u, v in edge_list: + coloring[frozenset([u, v])] = k + + E = { + frozenset([v_n_1, A_1[1]]), # spike + frozenset([v_n_1, A_1[0]]), # side-0 + frozenset([v_n_1, A_1[2]]), # side-1 + frozenset([A_1[3], A_1[4]]), # merged + } + + fig, ax = plt.subplots(figsize=(8, 8)) + draw(ax, G1, pos1, coloring=coloring, protected=E) + fig.savefig(os.path.join(OUT_DIR, 'fig_alg_step1.png'), + dpi=170, bbox_inches='tight') + plt.close(fig) + + # ----- Step 2: reduce at the only remaining safe face (outer pentagon) ----- + safe = find_safe_pentagonal_face(G1, E) + if safe is None: + print("ERROR: expected an outer pentagonal face but none found.") + return + boundary_2, externals_2, A_2 = safe + f_vec = [coloring[e] for e in externals_2] + choices = valid_indices(f_vec) + if not choices: + print(f"ERROR: f-vector {f_vec} has no valid index.") + return + i_t = choices[0] + + G2 = G1.copy() + for v in boundary_2: + G2.delete_vertex(v) + v_n_2 = ('v_n', 2) + G2.add_vertex(v_n_2) + G2.add_edge(v_n_2, A_2[i_t]) + G2.add_edge(v_n_2, A_2[(i_t + 1) % 5]) + G2.add_edge(v_n_2, A_2[(i_t + 2) % 5]) + G2.add_edge(A_2[(i_t + 3) % 5], A_2[(i_t + 4) % 5]) + G2.is_planar(set_embedding=True) + + coloring2 = {e: c for e, c in coloring.items() + if not any(u in boundary_2 for u in e)} + side_0_2 = frozenset([v_n_2, A_2[i_t]]) + spike_2 = frozenset([v_n_2, A_2[(i_t + 1) % 5]]) + side_1_2 = frozenset([v_n_2, A_2[(i_t + 2) % 5]]) + merged_2 = frozenset([A_2[(i_t + 3) % 5], A_2[(i_t + 4) % 5]]) + coloring2[side_0_2] = coloring[externals_2[i_t]] + coloring2[spike_2] = coloring[externals_2[(i_t + 1) % 5]] + coloring2[side_1_2] = coloring[externals_2[(i_t + 2) % 5]] + coloring2[merged_2] = coloring[externals_2[(i_t + 3) % 5]] + + pos2 = {v: p for v, p in pos1.items() if v not in boundary_2} + nbrs = [A_2[i_t], A_2[(i_t + 1) % 5], A_2[(i_t + 2) % 5]] + cx = sum(pos2[a][0] for a in nbrs) / 3 + cy = sum(pos2[a][1] for a in nbrs) / 3 + r = math.hypot(cx, cy) + # v_n^{(2)} lies outside the surviving graph (the deleted d's were outermost) + target_r = 5.0 + pos2[v_n_2] = (cx * target_r / r, cy * target_r / r) + + E |= {side_0_2, spike_2, side_1_2, merged_2} + + fig, ax = plt.subplots(figsize=(8, 8)) + draw(ax, G2, pos2, coloring=coloring2, protected=E) + fig.savefig(os.path.join(OUT_DIR, 'fig_alg_step2.png'), + dpi=170, bbox_inches='tight') + plt.close(fig) + + print(f"Wrote fig_alg_step{{0,1,2}}.png to {OUT_DIR}") + + +if __name__ == '__main__': + main() diff --git a/papers/dual_decomposition_minimal_counterexamples/experiments/iterated_reduction.py b/papers/dual_decomposition_minimal_counterexamples/experiments/iterated_reduction.py new file mode 100644 index 0000000..e1c5cba --- /dev/null +++ b/papers/dual_decomposition_minimal_counterexamples/experiments/iterated_reduction.py @@ -0,0 +1,238 @@ +"""Iterated reduced-dual reduction with protected edges (Sage). + +Implements Algorithm 3.1 from paper.tex: + + 0. G' = dual of G (a triangulation conjectured to be a minimal + counterexample). + 1. Apply Definition 2.1 to G' at a pentagonal face to get H_1; find a + proper 3-edge-colouring phi_1 of H_1. + 2. Initialise protected edge set E := {spike, side-0, side-1, merged} from + step 1. + 3. Iterate: find a pentagonal face of H_{t-1} whose 10 incident edges are + disjoint from E, pick a valid index i_t (Lemma 2.4), apply + Definition 2.1, extend phi_{t-1} to phi_t, and add the four new named + edges to E. + 4. Terminate when no safe pentagonal face exists. + +We run on the icosahedron-dodecahedron pair as a concrete trace; the +icosahedron is 4-colourable, so the dodecahedron is 3-edge-colourable and +the algorithm terminates combinatorially. + +Run with: + sage experiments/iterated_reduction.py +""" +from sage.all import Graph +from sage.graphs.graph_coloring import edge_coloring + + +# --------------------------------------------------------------------------- +# Build G' = dodecahedron with the same naming as experiments/reduced_dual.py: +# vertex families a (inner pentagon, will play the role of partial F_v's +# boundary vertices for the first reduction), b, c, d. +# --------------------------------------------------------------------------- +def build_dodecahedron(): + edges = [] + for i in range(5): + edges.append((('a', i), ('a', (i + 1) % 5))) # inner pentagon + edges.append((('a', i), ('b', i))) # spoke a-b + edges.append((('b', i), ('c', i))) # b-c + edges.append((('b', i), ('c', (i - 1) % 5))) # b-c (other side) + edges.append((('c', i), ('d', i))) # spoke c-d + edges.append((('d', i), ('d', (i + 1) % 5))) # outer pentagon + G = Graph(edges, multiedges=False, loops=False) + assert G.is_planar(set_embedding=True), "dodecahedron not planar?" + return G + + +# --------------------------------------------------------------------------- +# 3-edge-colour a cubic plane graph; return None if not 3-edge-colourable. +# --------------------------------------------------------------------------- +def proper_3_coloring(G): + classes = edge_coloring(G, value_only=False) + if len(classes) > 3: + return None + out = {} + for k, edge_list in enumerate(classes): + for u, v in edge_list: + out[frozenset([u, v])] = k + return out + + +# --------------------------------------------------------------------------- +# Face search: pentagonal face whose 10 incident edges are outside `protected`. +# Returns (boundary, externals, A) or None. +# --------------------------------------------------------------------------- +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] + # the external edge at each boundary vertex (the one not on the face) + externals = [] + 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: + # In a cubic graph each face-boundary vertex has exactly one + # external edge; otherwise something is off. + break + externals.append(frozenset([B_k, outer[0]])) + A.append(outer[0]) + else: + if not any(e in protected for e in boundary_edges + externals): + return boundary, externals, A + return None + + +# --------------------------------------------------------------------------- +# Lemma 2.4: any proper 3-edge-colouring forces the external vector at a +# pentagonal face to have shape (a, b, c, c, c) up to cyclic rotation. The +# valid index i for the reduction is one where positions i+3, i+4 host the +# doubled colour and positions i, i+1, i+2 host three distinct colours. +# --------------------------------------------------------------------------- +def valid_indices(f_vec): + out = [] + for i in range(5): + if f_vec[(i + 3) % 5] != f_vec[(i + 4) % 5]: + continue + triple = {f_vec[i], f_vec[(i + 1) % 5], f_vec[(i + 2) % 5]} + if len(triple) == 3: + out.append(i) + return out + + +# --------------------------------------------------------------------------- +# Apply Definition 2.1 at (F, i): delete the 5 boundary vertices, add v_n +# connected to A[i], A[i+1], A[i+2], add the chord A[i+3]-A[i+4]. Extend the +# colouring: every surviving edge keeps its colour; each new edge takes the +# colour of the deleted external at the same A_k (the unique third colour at +# A_k under the surviving edges). +# --------------------------------------------------------------------------- +def apply_reduction(G, boundary, externals, A, coloring, i, v_n_label): + G_new = G.copy() + for v in boundary: + G_new.delete_vertex(v) + G_new.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]) + G_new.add_edges([side_0, spike, side_1, merged]) + assert G_new.is_planar(set_embedding=True), "reduction broke planarity" + + coloring_new = { + e: c for e, c in coloring.items() if not any(u in boundary for u in e) + } + coloring_new[frozenset(side_0)] = coloring[externals[i]] + coloring_new[frozenset(spike)] = coloring[externals[(i + 1) % 5]] + coloring_new[frozenset(side_1)] = coloring[externals[(i + 2) % 5]] + coloring_new[frozenset(merged)] = coloring[externals[(i + 3) % 5]] + + named = { + 'spike': frozenset(spike), + 'side_0': frozenset(side_0), + 'side_1': frozenset(side_1), + 'merged': frozenset(merged), + } + return G_new, coloring_new, named + + +# --------------------------------------------------------------------------- +# Sanity check: verify that a coloring is proper (each vertex sees 3 colours). +# --------------------------------------------------------------------------- +def is_proper_3_coloring(G, coloring): + for v in G.vertex_iterator(): + seen = set() + for u in G.neighbor_iterator(v): + seen.add(coloring[frozenset([u, v])]) + if len(seen) != G.degree(v): + return False + return True + + +# --------------------------------------------------------------------------- +# Main driver. +# --------------------------------------------------------------------------- +def run_algorithm(max_iterations=50, verbose=True): + if verbose: + print("STEP 0: G' = dodecahedron (dual of the icosahedron)") + G_prime = build_dodecahedron() + if verbose: + print(f" |V(G')| = {G_prime.order()}, |E(G')| = {G_prime.size()}") + + # ---- STEP 1: apply Definition 2.1 to G' at the inner pentagon, i_1 = 0 + face_data = find_safe_pentagonal_face(G_prime, set()) + if face_data is None: + print(" No pentagonal face in G'.") + return + boundary, externals, A = face_data + + H = G_prime.copy() + for v in boundary: + H.delete_vertex(v) + v_n_label = ('v_n', 1) + H.add_vertex(v_n_label) + side_0 = (v_n_label, A[0]) + spike = (v_n_label, A[1]) + side_1 = (v_n_label, A[2]) + merged = (A[3], A[4]) + H.add_edges([side_0, spike, side_1, merged]) + assert H.is_planar(set_embedding=True) + + coloring = proper_3_coloring(H) + if coloring is None: + print(" H_1 is not 3-edge-colourable; algorithm halts.") + return + assert is_proper_3_coloring(H, coloring) + if verbose: + print(f"STEP 1: H_1 = reduced dual at the first face, i_1 = 0") + print(f" |V(H_1)| = {H.order()}, |E(H_1)| = {H.size()}; " + f"3-edge-coloured.") + + # ---- STEP 2: initialise the protected set + E = { + frozenset(spike), + frozenset(side_0), + frozenset(side_1), + frozenset(merged), + } + if verbose: + print(f"STEP 2: |E_protected| = {len(E)}") + + # ---- STEP 3-4: iterate + for t in range(2, max_iterations + 1): + face_data = find_safe_pentagonal_face(H, E) + if face_data is None: + if verbose: + print(f"\nTerminated at iteration t = {t}: " + f"no pentagonal face avoids E.") + break + boundary, externals, A = face_data + f_vec = [coloring[e] for e in externals] + choices = valid_indices(f_vec) + if not choices: + print(f" iter t = {t}: f-vector {f_vec} has no valid index " + f"(Lemma 2.4 should preclude this --- bug!)") + break + i_t = choices[0] + v_n_label = ('v_n', t) + H, coloring, named = apply_reduction( + H, boundary, externals, A, coloring, i_t, v_n_label) + assert is_proper_3_coloring(H, coloring) + E |= set(named.values()) + if verbose: + print(f" iter t = {t:>2}: f = {f_vec}, chose i_t = {i_t}; " + f"|V| = {H.order():>2}, |E_graph| = {H.size():>2}, " + f"|E_protected| = {len(E):>2}") + else: + if verbose: + print(f"\nReached max_iterations = {max_iterations}.") + + if verbose: + print(f"\nFinal H: |V| = {H.order()}, |E| = {H.size()}, " + f"|E_protected| = {len(E)}") + + +if __name__ == '__main__': + run_algorithm() diff --git a/papers/dual_decomposition_minimal_counterexamples/experiments/search_kempe_property.py b/papers/dual_decomposition_minimal_counterexamples/experiments/search_kempe_property.py new file mode 100644 index 0000000..0ab4496 --- /dev/null +++ b/papers/dual_decomposition_minimal_counterexamples/experiments/search_kempe_property.py @@ -0,0 +1,225 @@ +"""Search for a proper 3-edge-coloring of a reduced dual satisfying: + + (i) color(spike) == color(merged) + (ii) the {c_spike, c_side_0}-Kempe cycle through the spike contains + side_0 AND merged + (iii) the {c_spike, c_side_1}-Kempe cycle through the spike contains + side_1 AND merged + +Iterates over all min-degree-5 simple planar triangulations on n vertices +(via plantri through Sage), then every pentagonal face of the dual G', then +every index i in {0,...,4} for the reduced-dual construction, then every +proper 3-edge-coloring of the resulting reduced dual. Stops on the first hit. + +The icosahedron (n = 12) is the only n = 12 triangulation with min degree 5 +and was already known to fail (see check_dodecahedron_kempe.py). + +Run with: + sage experiments/search_kempe_property.py +""" +from sage.all import Graph +from sage.graphs.graph_generators import graphs +import sys +import time + + +def dual_of(G): + """Combinatorial dual of a planar G with the embedding set on G.""" + faces = G.faces() + edge_to_faces = {} + for fi, face in enumerate(faces): + for u, v in face: + e = frozenset((u, v)) + edge_to_faces.setdefault(e, []).append(fi) + dual_edges = [] + for e, fs in edge_to_faces.items(): + if len(fs) == 2: + dual_edges.append((fs[0], fs[1])) + return Graph(dual_edges, multiedges=False, loops=False) + + +def apply_reduction(G, face, i): + """Apply Definition 2.1 at the pentagonal `face` (list of directed edges) + with index i, returning (H, named) or (None, None) if the construction + breaks.""" + boundary = [u for (u, v) in face] + if len(set(boundary)) != 5: + return None, 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, None + A.append(outer[0]) + if len(set(A)) != 5: + return None, None + H = G.copy() + for v in boundary: + H.delete_vertex(v) + v_n = '__v_n__' + H.add_vertex(v_n) + side_0 = (v_n, A[i % 5]) + spike = (v_n, A[(i + 1) % 5]) + side_1 = (v_n, A[(i + 2) % 5]) + merged = (A[(i + 3) % 5], A[(i + 4) % 5]) + # If merged would be a self-loop or duplicate of an existing edge, skip + if A[(i + 3) % 5] == A[(i + 4) % 5]: + return None, None + H.add_edges([side_0, spike, side_1, merged]) + if H.has_multiple_edges() or H.has_loops(): + return None, None + if not H.is_planar(set_embedding=True): + return None, None + # Cubic check + if not all(H.degree(v) == 3 for v in H.vertex_iterator()): + return None, None + named = { + 'spike': frozenset(spike), + 'side_0': frozenset(side_0), + 'side_1': frozenset(side_1), + 'merged': frozenset(merged), + } + return H, named + + +def proper_3_edge_colorings(G): + edges = list(G.edges(labels=False)) + n_edges = len(edges) + adj = [[] for _ in range(n_edges)] + for i in range(n_edges): + 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_edges + + def back(k): + if k == n_edges: + yield tuple(coloring) + return + for c in range(3): + if all(coloring[j] != c for j in adj[k]): + coloring[k] = c + yield from back(k + 1) + coloring[k] = -1 + + return edges, back(0) + + +def kempe_cycle(edges, coloring, start_idx, color_pair): + a, b = color_pair + if coloring[start_idx] not in (a, b): + return None + in_sub = [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(edges, col, named_idx): + c_spike = col[named_idx['spike']] + c_merged = col[named_idx['merged']] + if c_spike != c_merged: + return False + c_s0 = col[named_idx['side_0']] + c_s1 = col[named_idx['side_1']] + kc0 = kempe_cycle(edges, col, named_idx['spike'], (c_spike, c_s0)) + if named_idx['side_0'] not in kc0 or named_idx['merged'] not in kc0: + return False + kc1 = kempe_cycle(edges, col, named_idx['spike'], (c_spike, c_s1)) + if named_idx['side_1'] not in kc1 or named_idx['merged'] not in kc1: + return False + return True + + +def report(edges, col, named_idx, named, info): + print() + print("*** MATCH FOUND ***") + for k, v in info.items(): + print(f" {k} = {v}") + print("Named edges and their colours:") + for role in ('spike', 'side_0', 'side_1', 'merged'): + e = edges[named_idx[role]] + print(f" {role:7s}: edge {tuple(e)}, colour {col[named_idx[role]]}") + print(f"Full coloring (indexed by edge order):") + for i, e in enumerate(edges): + print(f" [{col[i]}] {tuple(e)}") + + +def search(max_n=16, time_budget_sec=600): + start = time.time() + n = 12 + while n <= max_n: + 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)") + tcount = 0 + total_reductions = 0 + total_colorings = 0 + try: + it = graphs.triangulations(n, minimum_degree=5) + except Exception as ex: + print(f" cannot enumerate triangulations: {ex}") + n += 1 + continue + for G in it: + tcount += 1 + if not G.is_planar(set_embedding=True): + continue + D = dual_of(G) + if not D.is_planar(set_embedding=True): + continue + faces_D = D.faces() + pentagonal = [f for f in faces_D if len(f) == 5] + for face in pentagonal: + for i_red in range(5): + H, named = apply_reduction(D, face, i_red) + if H is None: + continue + total_reductions += 1 + edges, gen = proper_3_edge_colorings(H) + # Find indices of named edges + named_idx = {} + for ii, e in enumerate(edges): + es = frozenset((e[0], e[1])) + for role, ns in named.items(): + if es == ns: + named_idx[role] = ii + if len(named_idx) != 4: + continue + for col in gen: + total_colorings += 1 + if matches(edges, col, named_idx): + report(edges, col, named_idx, named, { + 'n': n, + 'triangulation_index': tcount, + 'face_size': len(face), + 'i_red': i_red, + 'reduced_dual_V': H.order(), + 'reduced_dual_E': H.size(), + }) + return + sys.stdout.flush() + print(f" n = {n}: {tcount} triangulation(s), " + f"{total_reductions} reductions, " + f"{total_colorings} colorings; no hit.") + n += 1 + print(f"\nSearch exhausted up to n = {max_n}.") + + +if __name__ == '__main__': + search() diff --git a/papers/dual_decomposition_minimal_counterexamples/fig_alg_step0.png b/papers/dual_decomposition_minimal_counterexamples/fig_alg_step0.png new file mode 100644 index 0000000..173879a Binary files /dev/null and b/papers/dual_decomposition_minimal_counterexamples/fig_alg_step0.png differ diff --git a/papers/dual_decomposition_minimal_counterexamples/fig_alg_step1.png b/papers/dual_decomposition_minimal_counterexamples/fig_alg_step1.png new file mode 100644 index 0000000..022f173 Binary files /dev/null and b/papers/dual_decomposition_minimal_counterexamples/fig_alg_step1.png differ diff --git a/papers/dual_decomposition_minimal_counterexamples/fig_alg_step2.png b/papers/dual_decomposition_minimal_counterexamples/fig_alg_step2.png new file mode 100644 index 0000000..77372f5 Binary files /dev/null and b/papers/dual_decomposition_minimal_counterexamples/fig_alg_step2.png differ diff --git a/papers/dual_decomposition_minimal_counterexamples/paper.aux b/papers/dual_decomposition_minimal_counterexamples/paper.aux index 2c8b4dc..0ea60b6 100644 --- a/papers/dual_decomposition_minimal_counterexamples/paper.aux +++ b/papers/dual_decomposition_minimal_counterexamples/paper.aux @@ -13,9 +13,15 @@ \@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces The proof of Lemma\nonbreakingspace 2.6\hbox {}, illustrated for $i = 0$ on $G' = $ the dodecahedron. Top: under the assumption $W \neq Y$, propriety at $v_n$ forces $W \in \{X, Z\}$. Bottom: in either case the lift to $G'$ has externals satisfying the hypothesis of Lemma\nonbreakingspace 2.4\hbox {}, which colours $\partial F_v$ to extend $\psi $ to a proper $3$-edge-colouring of $G'$.}}{5}{}\protected@file@percent } \newlabel{fig:chord-apex-proof}{{2}{5}} \newlabel{lem:kempe-spike}{{2.7}{6}} +\@writefile{toc}{\contentsline {section}{\tocsection {}{3}{An iterated reduction}}{7}{}\protected@file@percent } +\newlabel{alg:iterated-reduction}{{3.1}{7}} +\newlabel{rem:alg-invariants}{{3.2}{7}} +\newlabel{rem:alg-chord-apex}{{3.3}{7}} \newlabel{tocindent-1}{0pt} \newlabel{tocindent0}{0pt} \newlabel{tocindent1}{17.77782pt} \newlabel{tocindent2}{0pt} \newlabel{tocindent3}{0pt} -\gdef \@abspage@last{7} +\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Algorithm\nonbreakingspace 3.1\hbox {} on $G' = $ dodecahedron (dual of the icosahedron). \emph {Left:} $G'$ (20 vertices, 30 edges), with $F_v$ (the inner pentagon) shaded as the face chosen for the first reduction. \emph {Centre:} $H_1$ (16 vertices, 24 edges) after step\nonbreakingspace (1) with $i_1 = 0$, $3$-edge-coloured by Sage; the four edges around $v_n^{(1)}$ in $E$ are drawn thicker. \emph {Right:} $H_2$ (12 vertices, 18 edges) after step\nonbreakingspace (3) with $i_t = 0$; the only safe pentagonal face in $H_1$ was the outer pentagon, whose deletion produces $v_n^{(2)}$ and a second chord, giving eight protected edges. No safe pentagonal face remains, so the algorithm terminates. The generating script is \texttt {experiments/draw\_iterated\_reduction.py}.}}{8}{}\protected@file@percent } +\newlabel{fig:iterated-reduction-trace}{{3}{8}} +\gdef \@abspage@last{8} diff --git a/papers/dual_decomposition_minimal_counterexamples/paper.log b/papers/dual_decomposition_minimal_counterexamples/paper.log index 68afba2..2532749 100644 --- a/papers/dual_decomposition_minimal_counterexamples/paper.log +++ b/papers/dual_decomposition_minimal_counterexamples/paper.log @@ -1,4 +1,4 @@ -This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022) (preloaded format=pdflatex 2022.10.5) 23 MAY 2026 02:40 +This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022) (preloaded format=pdflatex 2022.10.5) 23 MAY 2026 03:21 entering extended mode restricted \write18 enabled. %&-line parsing enabled. @@ -144,26 +144,26 @@ File: l3backend-pdftex.def 2022-02-07 L3 backend support: PDF output (pdfTeX) (./paper.aux) \openout1 = `paper.aux'. -LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 25. -LaTeX Font Info: ... okay on input line 25. -LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 25. -LaTeX Font Info: ... okay on input line 25. -LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 25. -LaTeX Font Info: ... okay on input line 25. -LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 25. -LaTeX Font Info: ... okay on input line 25. -LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 25. -LaTeX Font Info: ... okay on input line 25. -LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 25. -LaTeX Font Info: ... okay on input line 25. -LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 25. -LaTeX Font Info: ... okay on input line 25. -LaTeX Font Info: Trying to load font information for U+msa on input line 25. +LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 26. +LaTeX Font Info: ... okay on input line 26. +LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 26. +LaTeX Font Info: ... okay on input line 26. +LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 26. +LaTeX Font Info: ... okay on input line 26. +LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 26. +LaTeX Font Info: ... okay on input line 26. +LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 26. +LaTeX Font Info: ... okay on input line 26. +LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 26. +LaTeX Font Info: ... okay on input line 26. +LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 26. +LaTeX Font Info: ... okay on input line 26. +LaTeX Font Info: Trying to load font information for U+msa on input line 26. (/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 25. +LaTeX Font Info: Trying to load font information for U+msb on input line 26. (/usr/local/texlive/2022/texmf-dist/tex/latex/amsfonts/umsb.fd @@ -192,7 +192,7 @@ 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}] -Overfull \hbox (41.917pt too wide) in paragraph at lines 143--145 +Overfull \hbox (41.917pt too wide) in paragraph at lines 144--146 []\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 )$. @@ -201,22 +201,22 @@ d $\OML/cmm/m/it/10 F$ \OT1/cmr/m/n/10 as $\OML/cmm/m/it/10 A \OT1/cmr/m/n/10 = File: fig_reduced_dual_step1.png Graphic file (type png) -Package pdftex.def Info: fig_reduced_dual_step1.png used on input line 163. +Package pdftex.def Info: fig_reduced_dual_step1.png used on input line 164. (pdftex.def) Requested size: 172.79846pt x 166.55775pt. File: fig_reduced_dual_step2.png Graphic file (type png) -Package pdftex.def Info: fig_reduced_dual_step2.png used on input line 164. +Package pdftex.def Info: fig_reduced_dual_step2.png used on input line 165. (pdftex.def) Requested size: 172.79846pt x 170.39505pt. File: fig_reduced_dual_step3.png Graphic file (type png) -Package pdftex.def Info: fig_reduced_dual_step3.png used on input line 165. +Package pdftex.def Info: fig_reduced_dual_step3.png used on input line 166. (pdftex.def) Requested size: 172.79846pt x 170.39505pt. File: fig_reduced_dual_step4.png Graphic file (type png) -Package pdftex.def Info: fig_reduced_dual_step4.png used on input line 166. +Package pdftex.def Info: fig_reduced_dual_step4.png used on input line 167. (pdftex.def) Requested size: 172.79846pt x 171.44409pt. LaTeX Warning: `h' float specifier changed to `ht'. @@ -226,50 +226,78 @@ uced_dual_step3.png> <./fig_reduced_dual_step4.png>] File: fig_chord_apex_step1.png Graphic file (type png) -Package pdftex.def Info: fig_chord_apex_step1.png used on input line 287. +Package pdftex.def Info: fig_chord_apex_step1.png used on input line 288. (pdftex.def) Requested size: 251.9989pt x 250.5104pt. File: fig_chord_apex_step2.png Graphic file (type png) -Package pdftex.def Info: fig_chord_apex_step2.png used on input line 288. +Package pdftex.def Info: fig_chord_apex_step2.png used on input line 289. (pdftex.def) Requested size: 172.79846pt x 176.08986pt. File: fig_chord_apex_step3.png Graphic file (type png) -Package pdftex.def Info: fig_chord_apex_step3.png used on input line 289. +Package pdftex.def Info: fig_chord_apex_step3.png used on input line 290. (pdftex.def) Requested size: 172.79846pt x 176.08986pt. 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] [7] (./paper.aux) ) -Here is how much of TeX's memory you used: - 3043 strings out of 478268 - 43156 string characters out of 5846347 - 343146 words of memory out of 5000000 - 21084 multiletter control sequences out of 15000+600000 - 476364 words of font info for 55 fonts, out of 8000000 for 9000 - 1302 hyphenation exceptions out of 8191 - 69i,8n,76p,664b,298s stack positions out of 10000i,1000n,20000p,200000b,200000s - -Output written on paper.pdf (7 pages, 755306 bytes). -PDF statistics: - 108 PDF objects out of 1000 (max. 8388607) - 58 compressed objects within 1 object stream - 0 named destinations out of 1000 (max. 500000) - 36 words of extra memory for PDF output out of 10000 (max. 10000000) +pex_step3.png>] [6] +Overfull \hbox (4.76643pt too wide) in paragraph at lines 432--439 +\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 )$ + [] + + +File: fig_alg_step0.png Graphic file (type png) + +Package pdftex.def Info: fig_alg_step0.png used on input line 478. +(pdftex.def) Requested size: 115.20264pt x 109.69525pt. + +File: fig_alg_step1.png Graphic file (type png) + +Package pdftex.def Info: fig_alg_step1.png used on input line 479. +(pdftex.def) Requested size: 115.20264pt x 109.69525pt. + +File: fig_alg_step2.png Graphic file (type png) + +Package pdftex.def Info: fig_alg_step2.png used on input line 480. +(pdftex.def) Requested size: 115.20264pt x 88.91956pt. +[7] [8 <./fig_alg_step0.png> <./fig_alg_step1.png> <./fig_alg_step2.png>] +(./paper.aux) ) +Here is how much of TeX's memory you used: + 3075 strings out of 478268 + 43781 string characters out of 5846347 + 343216 words of memory out of 5000000 + 21112 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,918b,298s stack positions out of 10000i,1000n,20000p,200000b,200000s + + +Output written on paper.pdf (8 pages, 983037 bytes). +PDF statistics: + 132 PDF objects out of 1000 (max. 8388607) + 69 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 f1cef5f..b52536f 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 fc39518..dd45950 100644 --- a/papers/dual_decomposition_minimal_counterexamples/paper.tex +++ b/papers/dual_decomposition_minimal_counterexamples/paper.tex @@ -16,6 +16,7 @@ \theoremstyle{definition} \newtheorem{definition}[theorem]{Definition} \newtheorem{example}[theorem]{Example} +\newtheorem{algorithm}[theorem]{Algorithm} \theoremstyle{remark} \newtheorem{remark}[theorem]{Remark} @@ -391,4 +392,103 @@ distinct colours, contradicting Lemma~\ref{lem:chord-apex} applied to $\varphi'$. \end{proof} +\section{An iterated reduction} + +The reduced-dual construction in Definition~\ref{def:reduced-dual} can be +iterated: starting from a proper $3$-edge-colouring $\varphi_1$ of a reduced +dual $\widehat{G}'_{v,i}$, we apply the construction again to that graph at +a pentagonal face whose ten incident edges avoid the four named edges from +the first reduction, extending $\varphi_1$ across the new reduction. The +protected edges accumulate into a set $E$ that grows by four per iteration, +and the process terminates when $E$ has blocked every pentagonal face. + +\begin{algorithm}[Iterated reduction with protected edges] +\label{alg:iterated-reduction} +Let $G$ be a triangulation we assume to be a minimal counterexample to the +Four Colour Theorem. The algorithm produces a sequence $H_1, H_2, \dots$ of +cubic plane graphs, proper $3$-edge-colourings $\varphi_t$ of $H_t$, and a +growing set $E$ of protected edges. + +\begin{enumerate} + \item[(0)] Form $G' := \mathrm{dual}(G)$, a cubic plane graph. + + \item[(1)] Choose a degree-$5$ vertex $v$ of $G$ (equivalently a pentagonal + face $F_v$ of $G'$) and an index $i_1 \in \{0, \dots, 4\}$. Apply + Definition~\ref{def:reduced-dual} to form + $H_1 := \widehat{G'}_{v, i_1}$, and fix any proper + $3$-edge-colouring $\varphi_1$ of $H_1$ (one exists by the minimality + of $G$). + + \item[(2)] Initialise $E := \{\text{spike}, \text{side-}0, \text{side-}1, + \text{merged}\}$, the four named edges of the reduction in (1). + + \item[(3)] (Iterate.) At step $t \geq 2$, given $H_{t-1}$, $\varphi_{t-1}$, + and $E \subseteq E(H_{t-1})$: + \begin{enumerate} + \item[(a)] Find a pentagonal face $F$ of $H_{t-1}$ whose ten + incident edges --- the five boundary edges of $\partial F$ + and the five external edges at $\partial F$ --- are all + outside $E$. If no such $F$ exists, terminate. + \item[(b)] By Lemma~\ref{lem:pentagonal-externals} applied to + $H_{t-1}$ at $F$ under $\varphi_{t-1}$, the external vector + has shape $(a, b, c, c, c)$ up to cyclic rotation. Choose an + index $i_t$ for which + $\varphi_{t-1}(f_{i_t + 3}) = \varphi_{t-1}(f_{i_t + 4})$ and + $\varphi_{t-1}(f_{i_t}), \varphi_{t-1}(f_{i_t + 1}), + \varphi_{t-1}(f_{i_t + 2})$ are three distinct colours. + \item[(c)] Apply Definition~\ref{def:reduced-dual} to $H_{t-1}$ at + $(F, i_t)$ to form $H_t$. + \item[(d)] Extend $\varphi_{t-1}$ to a proper $3$-edge-colouring + $\varphi_t$ of $H_t$: every surviving edge keeps its + $\varphi_{t-1}$-colour, and each new edge takes the unique + colour completing the palette at its endpoint (consistent + across both endpoints of the chord by the choice of $i_t$). + \item[(e)] Add the four named edges of the step-$t$ reduction to + $E$. + \end{enumerate} + + \item[(4)] Repeat (3) until termination. +\end{enumerate} +\end{algorithm} + +\begin{remark} +\label{rem:alg-invariants} +At each iteration, $|V(H_t)| = |V(H_{t-1})| - 4$ and +$|E(H_t)| = |E(H_{t-1})| - 6$, so $H_t$ shrinks at a fixed rate; the +protected set $|E|$ grows by exactly four; and every protected edge survives +all subsequent reductions. Since the graph is finite, termination is +guaranteed. By Lemma~\ref{lem:pentagonal-externals}, step~(b) never fails: +some valid $i_t$ always exists for any pentagonal face under any proper +colouring. Termination is therefore combinatorial: it occurs precisely when +$E$ touches every pentagonal face of $H_{t-1}$. +\end{remark} + +\begin{remark} +\label{rem:alg-chord-apex} +Lemma~\ref{lem:chord-apex} applies only at $t = 1$, when $H_1$ is a reduced +dual of $G'$. For $t \geq 2$, $H_t$ is a reduced dual of $H_{t-1}$ rather than +of $G'$, and $H_{t-1}$ is itself $3$-edge-colourable, so the +non-$3$-edge-colourability argument that drives Lemma~\ref{lem:chord-apex} +does not carry over. Whether the constraints accumulated in $E$ propagate +any further structure to $\varphi_t$ for $t \geq 2$ is left open. +\end{remark} + +\begin{figure}[h] +\centering +\includegraphics[width=0.32\textwidth]{fig_alg_step0.png}\hfill +\includegraphics[width=0.32\textwidth]{fig_alg_step1.png}\hfill +\includegraphics[width=0.32\textwidth]{fig_alg_step2.png} +\caption{Algorithm~\ref{alg:iterated-reduction} on $G' = $ dodecahedron +(dual of the icosahedron). \emph{Left:} $G'$ (20 vertices, 30 edges), with +$F_v$ (the inner pentagon) shaded as the face chosen for the first reduction. +\emph{Centre:} $H_1$ (16 vertices, 24 edges) after step~(1) with $i_1 = 0$, +$3$-edge-coloured by Sage; the four edges around $v_n^{(1)}$ in $E$ are drawn +thicker. \emph{Right:} $H_2$ (12 vertices, 18 edges) after step~(3) with +$i_t = 0$; the only safe pentagonal face in $H_1$ was the outer pentagon, +whose deletion produces $v_n^{(2)}$ and a second chord, giving eight protected +edges. No safe pentagonal face remains, so the algorithm terminates. The +generating script is \texttt{experiments/draw\_iterated\_reduction.py}.} +\label{fig:iterated-reduction-trace} +\end{figure} + \end{document}