face_monochromatic_pairs: rename check_conj_3_8_scaled → check_conj_final_scaled; add n=21-24 test

Rename the shared helper module to a number-resistant name. Update
all 26 dependent scripts via sed.

Add experiments/test_n_21_to_24.py — extends the empirical check
beyond |V(G)| ≤ 20 to n_G ∈ [21, 24]. Checks per chord-apex+Kempe
colouring:
  (1) h_φ constant on V(K_b)? (counterexample to Corollary 5.4)
  (2) h_φ constant on V(K_b) ∪ V(K_c)? (counterexample to Conj 5.1)
  (3) Deciding face exists?

Writes results incrementally to test_n_21_to_24_results.jsonl (one
JSON line per triangulation, plus n-level and grand summaries).
Emits PROGRESS lines every 10 minutes (default) to stdout for live
monitoring.

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

papers/face_monochromatic_pairs/experiments/characterize_S_vertices.py

@@ -28,7 +28,7 @@ from sage.graphs.graph_generators import graphs
 HERE = os.path.dirname(os.path.abspath(__file__))
 sys.path.insert(0, HERE)
 
-from check_conj_3_8_scaled import (
+from check_conj_final_scaled import (
     apply_reduction,
     proper_3_edge_colorings,
     matches_chord_apex_kempe,

papers/face_monochromatic_pairs/experiments/check_30_residual.py

@@ -29,7 +29,7 @@ from sage.graphs.graph_generators import graphs
 HERE = os.path.dirname(os.path.abspath(__file__))
 sys.path.insert(0, HERE)
 
-from check_conj_3_8_scaled import (
+from check_conj_final_scaled import (
     apply_reduction,
     proper_3_edge_colorings,
     matches_chord_apex_kempe,

papers/face_monochromatic_pairs/experiments/check_30_residual_v2.py

@@ -21,7 +21,7 @@ from sage.graphs.graph_generators import graphs
 HERE = os.path.dirname(os.path.abspath(__file__))
 sys.path.insert(0, HERE)
 
-from check_conj_3_8_scaled import (
+from check_conj_final_scaled import (
     apply_reduction,
     proper_3_edge_colorings,
     matches_chord_apex_kempe,

papers/face_monochromatic_pairs/experiments/check_S8_hit8_pG.py

@@ -17,7 +17,7 @@ from sage.graphs.graph_generators import graphs
 HERE = os.path.dirname(os.path.abspath(__file__))
 sys.path.insert(0, HERE)
 
-from check_conj_3_8_scaled import (
+from check_conj_final_scaled import (
     apply_reduction,
     proper_3_edge_colorings,
     matches_chord_apex_kempe,

papers/face_monochromatic_pairs/experiments/check_S_adjacency.py

@@ -21,7 +21,7 @@ from sage.graphs.graph_generators import graphs
 HERE = os.path.dirname(os.path.abspath(__file__))
 sys.path.insert(0, HERE)
 
-from check_conj_3_8_scaled import (
+from check_conj_final_scaled import (
     apply_reduction,
     proper_3_edge_colorings,
     matches_chord_apex_kempe,

papers/face_monochromatic_pairs/experiments/check_S_face_structure.py

@@ -23,7 +23,7 @@ from sage.graphs.graph_generators import graphs
 HERE = os.path.dirname(os.path.abspath(__file__))
 sys.path.insert(0, HERE)
 
-from check_conj_3_8_scaled import (
+from check_conj_final_scaled import (
     apply_reduction,
     proper_3_edge_colorings,
     matches_chord_apex_kempe,

papers/face_monochromatic_pairs/experiments/check_S_vs_pent_Fk.py

@@ -24,7 +24,7 @@ from sage.graphs.graph_generators import graphs
 HERE = os.path.dirname(os.path.abspath(__file__))
 sys.path.insert(0, HERE)
 
-from check_conj_3_8_scaled import (
+from check_conj_final_scaled import (
     apply_reduction,
     proper_3_edge_colorings,
     matches_chord_apex_kempe,

papers/face_monochromatic_pairs/experiments/check_bad_subcase_deciding_face.py

@@ -28,7 +28,7 @@ from sage.graphs.graph_generators import graphs
 HERE = os.path.dirname(os.path.abspath(__file__))
 sys.path.insert(0, HERE)
 
-from check_conj_3_8_scaled import (
+from check_conj_final_scaled import (
     apply_reduction,
     proper_3_edge_colorings,
     matches_chord_apex_kempe,

papers/face_monochromatic_pairs/experiments/check_c28_no_chord_apex_kempe_constancy.py

@@ -34,7 +34,7 @@ from sage.graphs.graph_generators import graphs
 HERE = os.path.dirname(os.path.abspath(__file__))
 sys.path.insert(0, HERE)
 
-from check_conj_3_8_scaled import (
+from check_conj_final_scaled import (
     apply_reduction,
     proper_3_edge_colorings,
     matches_chord_apex_kempe,

papers/face_monochromatic_pairs/experiments/check_conj_final_scaled.py

@@ -16,7 +16,7 @@ the 4-edge-face criterion). Then we:
          partial(f_n).
 Aggregates per-n.
 
-Run with: sage experiments/check_conj_3_8_scaled.py
+Run with: sage experiments/check_conj_final_scaled.py
 """
 from sage.all import Graph
 from sage.graphs.graph_generators import graphs

papers/face_monochromatic_pairs/experiments/check_conj_on_holton_mckay.py

@@ -7,7 +7,7 @@ Each Holton-McKay graph is itself a cubic plane graph $G'$; its dual is a
 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.
+Reuses the testing infrastructure from check_conj_final_scaled.py.
 
 Run with: sage experiments/check_conj_on_holton_mckay.py
 """
@@ -19,7 +19,7 @@ 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 (
+from check_conj_final_scaled import (
     apply_reduction,
     proper_3_edge_colorings,
     matches_chord_apex_kempe,

papers/face_monochromatic_pairs/experiments/check_constancy_obstruction.py

@@ -28,7 +28,7 @@ from sage.graphs.graph_generators import graphs
 HERE = os.path.dirname(os.path.abspath(__file__))
 sys.path.insert(0, HERE)
 
-from check_conj_3_8_scaled import (
+from check_conj_final_scaled import (
     apply_reduction,
     proper_3_edge_colorings,
     matches_chord_apex_kempe,

papers/face_monochromatic_pairs/experiments/check_cw_parity_prediction.py

@@ -31,7 +31,7 @@ from sage.graphs.graph_generators import graphs
 HERE = os.path.dirname(os.path.abspath(__file__))
 sys.path.insert(0, HERE)
 
-from check_conj_3_8_scaled import (
+from check_conj_final_scaled import (
     apply_reduction,
     proper_3_edge_colorings,
     matches_chord_apex_kempe,

papers/face_monochromatic_pairs/experiments/check_deciding_face.py

@@ -26,7 +26,7 @@ from sage.graphs.graph_generators import graphs
 HERE = os.path.dirname(os.path.abspath(__file__))
 sys.path.insert(0, HERE)
 
-from check_conj_3_8_scaled import (
+from check_conj_final_scaled import (
     apply_reduction,
     proper_3_edge_colorings,
     matches_chord_apex_kempe,

papers/face_monochromatic_pairs/experiments/check_gprime_pentagon_always_works.py

@@ -20,7 +20,7 @@ from sage.graphs.graph_generators import graphs
 HERE = os.path.dirname(os.path.abspath(__file__))
 sys.path.insert(0, HERE)
 
-from check_conj_3_8_scaled import (
+from check_conj_final_scaled import (
     apply_reduction,
     proper_3_edge_colorings,
     matches_chord_apex_kempe,

papers/face_monochromatic_pairs/experiments/check_heawood_local_side.py

@@ -28,7 +28,7 @@ from sage.graphs.graph_generators import graphs
 HERE = os.path.dirname(os.path.abspath(__file__))
 sys.path.insert(0, HERE)
 
-from check_conj_3_8_scaled import (
+from check_conj_final_scaled import (
     apply_reduction,
     proper_3_edge_colorings,
     matches_chord_apex_kempe,

papers/face_monochromatic_pairs/experiments/check_heawood_on_kempe.py

@@ -22,7 +22,7 @@ from sage.graphs.graph_generators import graphs
 HERE = os.path.dirname(os.path.abspath(__file__))
 sys.path.insert(0, HERE)
 
-from check_conj_3_8_scaled import (
+from check_conj_final_scaled import (
     apply_reduction,
     proper_3_edge_colorings,
     matches_chord_apex_kempe,

papers/face_monochromatic_pairs/experiments/check_heawood_pair_mismatch.py

@@ -23,7 +23,7 @@ from sage.graphs.graph_generators import graphs
 HERE = os.path.dirname(os.path.abspath(__file__))
 sys.path.insert(0, HERE)
 
-from check_conj_3_8_scaled import (
+from check_conj_final_scaled import (
     apply_reduction,
     proper_3_edge_colorings,
     matches_chord_apex_kempe,

papers/face_monochromatic_pairs/experiments/check_heawood_per_kempe_cycle.py

@@ -18,7 +18,7 @@ from sage.graphs.graph_generators import graphs
 HERE = os.path.dirname(os.path.abspath(__file__))
 sys.path.insert(0, HERE)
 
-from check_conj_3_8_scaled import (
+from check_conj_final_scaled import (
     apply_reduction,
     proper_3_edge_colorings,
     matches_chord_apex_kempe,

papers/face_monochromatic_pairs/experiments/check_heawood_side_correlation.py

@@ -24,7 +24,7 @@ from sage.graphs.graph_generators import graphs
 HERE = os.path.dirname(os.path.abspath(__file__))
 sys.path.insert(0, HERE)
 
-from check_conj_3_8_scaled import (
+from check_conj_final_scaled import (
     apply_reduction,
     proper_3_edge_colorings,
     matches_chord_apex_kempe,

papers/face_monochromatic_pairs/experiments/check_kb_kc_coverage.py

@@ -21,7 +21,7 @@ from sage.graphs.graph_generators import graphs
 HERE = os.path.dirname(os.path.abspath(__file__))
 sys.path.insert(0, HERE)
 
-from check_conj_3_8_scaled import (
+from check_conj_final_scaled import (
     apply_reduction,
     proper_3_edge_colorings,
     matches_chord_apex_kempe,

papers/face_monochromatic_pairs/experiments/check_kempe_intersection_and_alternation.py

@@ -33,7 +33,7 @@ from sage.graphs.graph_generators import graphs
 HERE = os.path.dirname(os.path.abspath(__file__))
 sys.path.insert(0, HERE)
 
-from check_conj_3_8_scaled import (
+from check_conj_final_scaled import (
     apply_reduction,
     proper_3_edge_colorings,
     matches_chord_apex_kempe,

papers/face_monochromatic_pairs/experiments/check_min_flip_structure.py

@@ -21,7 +21,7 @@ from sage.graphs.graph_generators import graphs
 HERE = os.path.dirname(os.path.abspath(__file__))
 sys.path.insert(0, HERE)
 
-from check_conj_3_8_scaled import (
+from check_conj_final_scaled import (
     apply_reduction,
     proper_3_edge_colorings,
     matches_chord_apex_kempe,

papers/face_monochromatic_pairs/experiments/check_minority_location.py

@@ -21,7 +21,7 @@ from sage.graphs.graph_generators import graphs
 HERE = os.path.dirname(os.path.abspath(__file__))
 sys.path.insert(0, HERE)
 
-from check_conj_3_8_scaled import (
+from check_conj_final_scaled import (
     apply_reduction,
     proper_3_edge_colorings,
     matches_chord_apex_kempe,

papers/face_monochromatic_pairs/experiments/check_shared_parity.py

@@ -24,7 +24,7 @@ from sage.graphs.graph_generators import graphs
 HERE = os.path.dirname(os.path.abspath(__file__))
 sys.path.insert(0, HERE)
 
-from check_conj_3_8_scaled import (
+from check_conj_final_scaled import (
     apply_reduction,
     proper_3_edge_colorings,
     matches_chord_apex_kempe,

papers/face_monochromatic_pairs/experiments/check_shared_sequence_and_winding.py

@@ -24,7 +24,7 @@ from sage.graphs.graph_generators import graphs
 HERE = os.path.dirname(os.path.abspath(__file__))
 sys.path.insert(0, HERE)
 
-from check_conj_3_8_scaled import (
+from check_conj_final_scaled import (
     apply_reduction,
     proper_3_edge_colorings,
     matches_chord_apex_kempe,

papers/face_monochromatic_pairs/experiments/check_subcase_iib.py

@@ -33,7 +33,7 @@ from sage.graphs.graph_generators import graphs
 HERE = os.path.dirname(os.path.abspath(__file__))
 sys.path.insert(0, HERE)
 
-from check_conj_3_8_scaled import (
+from check_conj_final_scaled import (
     apply_reduction,
     proper_3_edge_colorings,
     matches_chord_apex_kempe,

papers/face_monochromatic_pairs/experiments/test_n_21_to_24.py

@@ -0,0 +1,252 @@
+"""Test Conjecture 5.1 (face-monochromatic-pair) on chord-apex+Kempe
+colourings of reduced duals for n in [21, 24].
+
+For each (G, v, i, φ) chord-apex+Kempe colouring, check:
+  (1) Is h_φ constant on V(K_b) ∪ V(K_c)? (= potential counterexample
+      to Conjecture 5.1)
+  (2) Is h_φ constant on V(K_b) alone? (= weaker condition, would
+      contradict Corollary 5.4)
+  (3) Does a deciding face exist (∂f ⊆ V(K_b) ∪ V(K_c) and |f| ≢ 0
+      mod 3)? (= condition for the structural proof to apply)
+
+The known empirical result for n ≤ 20 is 0/142,812 for (1) and (2),
+and 142,812/142,812 for (3). We extend to n = 21, 22, 23, 24.
+
+Results are written incrementally to results.jsonl in the cwd, so
+that partial progress is preserved if the script is interrupted.
+
+The script also prints PROGRESS lines (= one per triangulation
+processed, or every 10 minutes elapsed, whichever first) that can
+be tailed for live monitoring.
+
+Run with: sage experiments/test_n_21_to_24.py
+"""
+import json
+import os
+import sys
+import time
+from pathlib import Path
+
+from sage.all import Graph
+from sage.graphs.graph_generators import graphs
+
+HERE = os.path.dirname(os.path.abspath(__file__))
+sys.path.insert(0, HERE)
+
+from check_conj_final_scaled import (
+    apply_reduction,
+    proper_3_edge_colorings,
+    matches_chord_apex_kempe,
+    kempe_cycle_set,
+    edge_idx,
+)
+from check_heawood_on_kempe import dual_of, heawood_numbers, vertices_of_kempe
+
+
+RESULTS_FILE = Path(HERE) / '..' / 'test_n_21_to_24_results.jsonl'
+
+
+def find_deciding_face(H, V_union):
+    """Return (face, |face|) for some deciding face, or None."""
+    for f in H.faces():
+        verts = {u for (u, v) in f} | {v for (u, v) in f}
+        if not verts.issubset(V_union):
+            continue
+        L = len(f)
+        if L % 3 != 0:
+            return f, L
+    return None
+
+
+def test_one(D):
+    """For a given dual D, iterate reductions + chord-apex+Kempe
+    colourings, return a dict of counters."""
+    D.is_planar(set_embedding=True)
+    n_col = 0
+    n_const_kb = 0
+    n_const_kb_kc_union = 0
+    n_no_deciding = 0
+    n_counterexamples = []   # save details of any counterexample
+    for face in D.faces():
+        if len(face) != 5: continue
+        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_col += 1
+                try:
+                    h = heawood_numbers(H, edges, col)
+                except RuntimeError:
+                    continue
+                merged_idx = edge_idx(edges, named['merged'])
+                a = col[merged_idx]
+                bs = [c for c in range(3) if c != a]
+                kc_b = kempe_cycle_set(edges, col, merged_idx, (a, bs[0]))
+                kc_c = kempe_cycle_set(edges, col, merged_idx, (a, bs[1]))
+                V_b = vertices_of_kempe(edges, kc_b)
+                V_c = vertices_of_kempe(edges, kc_c)
+                V_union = V_b | V_c
+                # Check constancy
+                h_b_vals = {h[v] for v in V_b}
+                h_union_vals = {h[v] for v in V_union}
+                if len(h_b_vals) == 1:
+                    n_const_kb += 1
+                    n_counterexamples.append({
+                        'type': 'const_kb',
+                        'n_V_b': len(V_b),
+                    })
+                if len(h_union_vals) == 1:
+                    n_const_kb_kc_union += 1
+                    n_counterexamples.append({
+                        'type': 'const_union',
+                        'n_V_union': len(V_union),
+                    })
+                # Check deciding face
+                dec = find_deciding_face(H, V_union)
+                if dec is None:
+                    n_no_deciding += 1
+                    n_counterexamples.append({
+                        'type': 'no_deciding',
+                        'n_V_union': len(V_union),
+                    })
+    return n_col, n_const_kb, n_const_kb_kc_union, n_no_deciding, n_counterexamples
+
+
+def write_result(record):
+    """Append a single JSONL record."""
+    with open(RESULTS_FILE, 'a') as f:
+        f.write(json.dumps(record) + '\n')
+        f.flush()
+
+
+def main(n_min=21, n_max=24, progress_every_seconds=600):
+    started_at = time.time()
+    # Clear / create the results file
+    print(f"Writing incremental results to {RESULTS_FILE}")
+    print(f"PROGRESS lines emitted every {progress_every_seconds}s "
+          f"(in addition to per-triangulation logs)")
+    sys.stdout.flush()
+    if RESULTS_FILE.exists():
+        # Preserve old log under .bak; new run starts fresh
+        bak = RESULTS_FILE.with_suffix(RESULTS_FILE.suffix + '.bak')
+        RESULTS_FILE.rename(bak)
+        print(f"Previous results moved to {bak}")
+    RESULTS_FILE.touch()
+
+    grand_col = 0
+    grand_const_kb = 0
+    grand_const_union = 0
+    grand_no_deciding = 0
+
+    last_progress = time.time()
+
+    for n in range(n_min, n_max + 1):
+        n_start = time.time()
+        print(f"\n=== n_G = {n} ===")
+        sys.stdout.flush()
+        try:
+            triangulations_iter = graphs.triangulations(n, minimum_degree=5)
+        except Exception as ex:
+            print(f"n={n}: cannot enumerate ({ex})")
+            continue
+        n_col_n = 0
+        n_const_kb_n = 0
+        n_const_union_n = 0
+        n_no_deciding_n = 0
+        tri_idx = 0
+        for G in triangulations_iter:
+            G.is_planar(set_embedding=True)
+            D = dual_of(G)
+            tri_start = time.time()
+            nc, nck, ncu, nnd, examples = test_one(D)
+            tri_elapsed = time.time() - tri_start
+            n_col_n += nc
+            n_const_kb_n += nck
+            n_const_union_n += ncu
+            n_no_deciding_n += nnd
+            # Write per-triangulation record
+            record = {
+                'n_G': n, 'tri_idx': tri_idx,
+                'n_col': nc,
+                'n_const_kb': nck,
+                'n_const_kb_kc_union': ncu,
+                'n_no_deciding': nnd,
+                'tri_elapsed_s': round(tri_elapsed, 2),
+                'wall_elapsed_s': round(time.time() - started_at, 2),
+                'examples': examples,
+            }
+            write_result(record)
+            # Time-based progress line
+            now = time.time()
+            if now - last_progress >= progress_every_seconds:
+                wall_min = (now - started_at) / 60
+                print(f"PROGRESS: wall {wall_min:.1f} min; "
+                      f"n={n} tri {tri_idx+1} done ({tri_elapsed:.1f}s); "
+                      f"running totals @n={n}: col={n_col_n}, "
+                      f"const_kb={n_const_kb_n}, "
+                      f"const_union={n_const_union_n}, "
+                      f"no_dec={n_no_deciding_n}")
+                sys.stdout.flush()
+                last_progress = now
+            tri_idx += 1
+
+        n_elapsed = time.time() - n_start
+        # n-level summary record
+        summary = {
+            'type': 'n_summary',
+            'n_G': n,
+            'n_tri': tri_idx,
+            'n_col': n_col_n,
+            'n_const_kb': n_const_kb_n,
+            'n_const_kb_kc_union': n_const_union_n,
+            'n_no_deciding': n_no_deciding_n,
+            'n_elapsed_s': round(n_elapsed, 2),
+            'wall_elapsed_s': round(time.time() - started_at, 2),
+        }
+        write_result(summary)
+        print(f"\nn={n}: {tri_idx} triangulations, {n_col_n} colourings "
+              f"[{n_elapsed:.0f}s]")
+        print(f"  const_kb: {n_const_kb_n}")
+        print(f"  const_kb_kc_union: {n_const_union_n}")
+        print(f"  no_deciding_face: {n_no_deciding_n}")
+        sys.stdout.flush()
+
+        grand_col += n_col_n
+        grand_const_kb += n_const_kb_n
+        grand_const_union += n_const_union_n
+        grand_no_deciding += n_no_deciding_n
+
+    total_elapsed = time.time() - started_at
+    final = {
+        'type': 'grand_summary',
+        'n_min': n_min, 'n_max': n_max,
+        'grand_col': grand_col,
+        'grand_const_kb': grand_const_kb,
+        'grand_const_kb_kc_union': grand_const_union,
+        'grand_no_deciding': grand_no_deciding,
+        'wall_elapsed_s': round(total_elapsed, 2),
+    }
+    write_result(final)
+    print("\n" + "=" * 70)
+    print(f"DONE: n in [{n_min}, {n_max}], "
+          f"{grand_col} chord-apex+Kempe colourings tested "
+          f"in {total_elapsed/60:.1f} min")
+    print(f"  const_kb: {grand_const_kb}")
+    print(f"  const_kb_kc_union: {grand_const_union}")
+    print(f"  no_deciding_face: {grand_no_deciding}")
+    if (grand_const_kb == 0 and grand_const_union == 0
+            and grand_no_deciding == 0):
+        print("✓ Conjecture 5.1 + Deciding-face conjecture EMPIRICALLY "
+              "EXTENDED to n_G ≤ {}".format(n_max))
+
+
+if __name__ == '__main__':
+    import sys
+    n_min = int(sys.argv[1]) if len(sys.argv) > 1 else 21
+    n_max = int(sys.argv[2]) if len(sys.argv) > 2 else 24
+    main(n_min=n_min, n_max=n_max)