dual_decomposition: verify strengthened conjecture on 6 Holton-McKay duals

- New experiment experiments/check_conj_on_holton_mckay.py parses
  McKay's planar_code file of the 6 non-Hamiltonian 38-vertex cubic
  plane graphs (Holton-McKay) and tests both clauses (1)-(3) and (1)-(4)
  of the face-monochromatic-pair conjecture on each. Result: 17,280
  candidate colourings, all 17,280 satisfy both conjectures.
- Add a "Targeted check on the Holton-McKay duals" paragraph to
  Remark 4.4 with a per-graph table.
- Fix a latent bug in check_conj_3_8_scaled.py: b was hardcoded to
  cyc_b, leaving b == a when phi(e_1) == cyc_b (and consequently c
  ambiguous). Now correctly computes b = whichever of cyc_a/cyc_b is
  not a, raising if neither matches. The bug never crashed n <= 20
  because any() short-circuited on correctly-built witnesses; the
  Holton-McKay reductions hit it on the first witness, surfacing it.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

papers/dual_decomposition_minimal_counterexamples/experiments/check_conj_3_8_scaled.py

@@ -190,13 +190,19 @@ def check_clause_4(H, edges, col_list, named, witness):
     """Construct the modified H + recoloring, identify f_n, check clause 4."""
     e1, e2 = witness['e1'], witness['e2']
     e_F = witness['e_F']
-    a = col_list[e1]    # color of e_1 = e_2
+    a = col_list[e1]    # color of e_1 = e_2 (clauses 1)
     merged_idx = edge_idx(edges, named['merged'])
     cyc_a, cyc_b = witness['kc_color_pair']   # = (c_merged, c_other)
-    # a is the colour of e_1, e_2 on the Kempe cycle. By chord-apex,
+    # On the {cyc_a, cyc_b}-Kempe cycle, e_1 carries colour a, which
-    # c_merged is the color of merged = the color of all "a"-edges on the
+    # equals either cyc_a or cyc_b. The conjecture's "b" is the OTHER
-    # cycle. The cycle alternates between c_merged = a and c_other = b.
+    # colour on the cycle; we set it accordingly.
-    b = cyc_b
+    if a == cyc_a:
+        b = cyc_b
+    elif a == cyc_b:
+        b = cyc_a
+    else:
+        raise RuntimeError(
+            f"e_1 colour {a} not in Kempe pair {(cyc_a, cyc_b)}")
     c = ({0, 1, 2} - {a, b}).pop()
 
     # Subdivided cycle K' alternates blue/green starting from merged = blue

papers/dual_decomposition_minimal_counterexamples/experiments/check_conj_on_holton_mckay.py

@@ -0,0 +1,131 @@
+"""Test the face-monochromatic-pair conjecture (both the weak form,
+clauses 1-3, and the strengthening, clauses 1-4) on the 6 duals of the
+non-Hamiltonian 38-vertex cubic plane graphs found by Holton & McKay.
+
+Each Holton-McKay graph is itself a cubic plane graph $G'$; its dual is a
+21-vertex triangulation $G$. We treat each Holton-McKay graph as the $G'$
+of a hypothetical minimal counterexample and apply the reduced-dual
+construction at each of its pentagonal faces.
+
+Reuses the testing infrastructure from check_conj_3_8_scaled.py.
+
+Run with: sage experiments/check_conj_on_holton_mckay.py
+"""
+import os
+import sys
+
+from sage.all import Graph
+
+HERE = os.path.dirname(os.path.abspath(__file__))
+sys.path.insert(0, HERE)
+
+from check_conj_3_8_scaled import (
+    apply_reduction,
+    proper_3_edge_colorings,
+    matches_chord_apex_kempe,
+    find_all_36_witnesses,
+    check_clause_4,
+)
+from check_conj_face_kempe_scaled import conjecture_holds_for
+
+
+HM_FILE = ('/Users/didericis/Code/math-research/papers/'
+           'even_level_graph_generators/experiments/nonham38m4.pc')
+
+
+def parse_planar_code_to_sage(path):
+    """Parse McKay's planar_code file and return list of Sage Graphs (each
+    a 3-connected cubic plane graph)."""
+    with open(path, 'rb') as f:
+        data = f.read()
+    header = b'>>planar_code<<'
+    assert data.startswith(header), data[:20]
+    pos = len(header)
+    sage_graphs = []
+    while pos < len(data):
+        n = data[pos]; pos += 1
+        edges = set()
+        for v in range(n):
+            while True:
+                w = data[pos]; pos += 1
+                if w == 0:
+                    break
+                edges.add(frozenset((v, w - 1)))
+        G = Graph([tuple(e) for e in edges], multiedges=False, loops=False)
+        G.is_planar(set_embedding=True)
+        sage_graphs.append(G)
+    return sage_graphs
+
+
+def test_one(D, name=""):
+    """Test conjecture on one cubic plane graph $D$ ($= G'$). Returns
+    (n_cand, n_sat_123, n_sat_1234, faces_used, indices_used)."""
+    D.is_planar(set_embedding=True)
+    n_cand = n_sat_123 = n_sat_1234 = 0
+    face_count = 0
+    for face in D.faces():
+        if len(face) != 5:
+            continue
+        face_count += 1
+        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)]
+            for col in cand:
+                n_cand += 1
+                if conjecture_holds_for(H, edges, col, named):
+                    n_sat_123 += 1
+                # clauses 1-4: existential at the witness level
+                witnesses = find_all_36_witnesses(H, edges, col, named)
+                if any(check_clause_4(H, edges, col, named, w)
+                       for w in witnesses):
+                    n_sat_1234 += 1
+    return n_cand, n_sat_123, n_sat_1234, face_count
+
+
+def main():
+    graphs_list = parse_planar_code_to_sage(HM_FILE)
+    print(f"Loaded {len(graphs_list)} Holton-McKay graphs from "
+          f"{HM_FILE}\n")
+
+    grand_cand = grand_123 = grand_1234 = 0
+    rows = []
+    import time
+    for i, G in enumerate(graphs_list):
+        n = G.order()
+        m = G.size()
+        degs = sorted(set(G.degree()))
+        t0 = time.time()
+        n_cand, n_123, n_1234, n_pent = test_one(G, name=f"HM{i}")
+        dt = time.time() - t0
+        rows.append((i, n, m, degs, n_pent, n_cand, n_123, n_1234, dt))
+        grand_cand += n_cand
+        grand_123 += n_123
+        grand_1234 += n_1234
+        sys_stdout = sys.stdout
+        print(f"HM{i}: n={n} m={m} deg={degs} pent_faces={n_pent} "
+              f"cand={n_cand} sat(1-3)={n_123} sat(1-4)={n_1234} "
+              f"[{dt:.1f}s]")
+        sys.stdout.flush()
+
+    print()
+    print("=" * 78)
+    print(f"{'i':>2} {'n':>3} {'m':>4} {'#pent':>6} {'#cand':>8} "
+          f"{'#sat(1-3)':>10} {'#sat(1-4)':>10} {'time':>7}")
+    print("-" * 78)
+    for i, n, m, degs, n_pent, n_cand, n_123, n_1234, dt in rows:
+        print(f"{i:>2} {n:>3} {m:>4} {n_pent:>6} {n_cand:>8} "
+              f"{n_123:>10} {n_1234:>10} {dt:>6.1f}s")
+    print("-" * 78)
+    print(f"{'tot':>2} {'-':>3} {'-':>4} {'-':>6} {grand_cand:>8} "
+          f"{grand_123:>10} {grand_1234:>10}")
+
+
+if __name__ == '__main__':
+    main()

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)  24 MAY 2026 14:32
+This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022) (preloaded format=pdflatex 2022.10.5)  24 MAY 2026 14:42
 entering extended mode
  restricted \write18 enabled.
  %&-line parsing enabled.
@@ -310,7 +310,7 @@ cal/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/loc
 al/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8.pfb></usr/local
 /texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb></usr/local/
 texlive/2022/texmf-dist/fonts/type1/public/amsfonts/symbols/msam10.pfb>
-Output written on paper.pdf (12 pages, 1015233 bytes).
+Output written on paper.pdf (12 pages, 1017869 bytes).
 PDF statistics:
  183 PDF objects out of 1000 (max. 8388607)
  101 compressed objects within 2 object streams

papers/dual_decomposition_minimal_counterexamples/paper.tex

@@ -745,6 +745,31 @@ Conjecture-\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}-witnesses
 individually satisfy clause~(4) on each colouring, but in every case
 \emph{some} witness does. Clause~(4) is therefore an existential statement
 at the witness level, not a property of every witness.
+
+\smallskip\noindent\emph{Targeted check on the Holton--McKay duals.}
+The six $21$-vertex triangulations whose duals are the
+non-Hamiltonian $38$-vertex cubic plane graphs of Holton and McKay
+(the smallest examples falsifying Tait's conjecture) are a particularly
+interesting subfamily at $n = 21$. Running the strengthened test directly
+on these six (see
+\texttt{experiments/check\_conj\_on\_holton\_mckay.py}) gives:
+
+\begin{center}
+\small
+\renewcommand{\arraystretch}{1.15}
+\begin{tabular}{r|r|r|r|l}
+HM\# & \#pentagonal faces & \#col.\ tested & \#sat.\ (1)--(4) & status \\
+\hline
+$0$ & $10$ & $2{,}880$ & $2{,}880$ & all pass \\
+$1$ & $11$ & $2{,}880$ & $2{,}880$ & all pass \\
+$2$ & $10$ & $2{,}880$ & $2{,}880$ & all pass \\
+$3$ & $10$ & $2{,}880$ & $2{,}880$ & all pass \\
+$4$ & $11$ & $2{,}880$ & $2{,}880$ & all pass \\
+$5$ & $11$ & $2{,}880$ & $2{,}880$ & all pass \\
+\hline
+total & --- & $17{,}280$ & $17{,}280$ & \\
+\end{tabular}
+\end{center}
 \end{remark}
 
 \begin{remark}[The implication to the Four Colour Theorem]