face_monochromatic_pairs: empirical check on flank-adjacent neighbour degrees

experiments/check_v_neighbour_degrees.py reports the cyclic degree
sequence of v's 5 neighbours in G across all (G, v, i) triples
underlying chord-apex+Kempe colourings (|V(G)| ≤ 20).

Result:
  - 100.00% of (G, v) pairs have at least one neighbour of v of
    degree 5. So the partial proof of the deciding-face conjecture
    (Theorem deciding-face-partial, which requires n_k ∈ {5, 6} for
    some k) handles all (G, v) pairs IF we can pick any k freely.
  - 99.70% of (G, v, i) triples have min(n_i, n_{i+1}) ≤ 6, so the
    partial proof's flank-face argument applies to the specific i.
  - 24 / 7,930 (0.30%) triples have BOTH n_i ≥ 7 AND n_{i+1} ≥ 7
    (the "bad" case where the partial proof's flank-face doesn't
    work). These occur at n_G = 19, 20 for triangulations with
    cyclic neighbour-degree sequences like (5,7,7,5,5).

For these 24 bad triples, the remaining 3 neighbours typically have
degree 5, so F^♭_outer (length n_{i+2} + n_{i+4} - 3 = 5+5-3 = 7,
not divisible by 3) becomes the candidate deciding face. Extending
the structural proof to cover F^♭_outer is the next step.

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

papers/face_monochromatic_pairs/experiments/check_v_neighbour_degrees.py

@@ -0,0 +1,147 @@
+"""For every reduction (G, v, i) underlying a chord-apex+Kempe
+colouring (up to |V(G)| ≤ 20), check the degrees of v's five
+neighbours in G.
+
+This determines whether the partial structural proof of the
+deciding-face conjecture (Theorem~\\ref{thm:deciding-face-partial} in
+the paper) covers ALL configurations empirically:
+
+  - If every (G, v) we encounter has at least one neighbour of v with
+    deg_G(·) ≤ 6, the partial proof (which requires at least one
+    n_k ∈ {5, 6}, equivalently at least one u_{k+1} with deg_G ≤ 6)
+    handles every chord-apex+Kempe colouring up to |V(G)| ≤ 20.
+
+  - If some (G, v) has all five neighbours of degree ≥ 7, we'd need
+    the unproved merged-side argument for those.
+
+Reports per n_G: number of (G, v) pairs with all-≥-7 neighbours.
+
+Run with: sage experiments/check_v_neighbour_degrees.py
+"""
+import os
+import sys
+import time
+
+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)
+
+
+def cyclic_neighbour_degrees(G, v):
+    """Return the cyclic sequence of degrees of v's neighbours, in
+    their CW order around v in G's planar embedding."""
+    G.is_planar(set_embedding=True)
+    emb = G.get_embedding()
+    return [G.degree(u) for u in emb[v]]
+
+
+def main(max_n=20, time_budget_per_n=1200):
+    print("For every (G, v, i) underlying a chord-apex+Kempe colouring, "
+          "check the\ndegrees of v's neighbours in G.\n")
+    print("Each reduction index i ∈ {0,…,4} picks two consecutive "
+          "neighbours\n(u_{i+1}, u_{i+2}) of v whose degrees become the\n"
+          "two flank-face adjacent G'-face lengths n_i, n_{i+1}.\n")
+    print(f"n_G in [12, {max_n}]\n")
+
+    grand_triples = 0           # total (G, v, i) triples
+    grand_bad_triples = 0       # both n_i, n_{i+1} ≥ 7
+    grand_pairs = 0             # (G, v) pairs
+    grand_all_ge_7 = 0          # (G, v) pairs with all 5 neighbours deg ≥ 7
+    grand_dist_min = {}         # min neighbour deg over (G, v)
+    grand_dist_consec = {}      # min over consecutive pair (n_i, n_{i+1}) for some i
+    grand_examples = []
+
+    for n in range(12, max_n + 1):
+        start = time.time()
+        try:
+            triangulations = list(graphs.triangulations(n, minimum_degree=5))
+        except Exception as ex:
+            print(f"n={n}: cannot enumerate ({ex})")
+            continue
+        triples_n = 0
+        bad_triples_n = 0
+        pairs_n = 0
+        all_ge_7_n = 0
+        for tri_idx, G in enumerate(triangulations):
+            if time.time() - start > time_budget_per_n:
+                print(f"  n={n}: timeout at tri {tri_idx}/{len(triangulations)}")
+                break
+            for v in G.vertex_iterator():
+                if G.degree(v) != 5:
+                    continue
+                cyc = cyclic_neighbour_degrees(G, v)
+                pairs_n += 1
+                m_all = min(cyc)
+                grand_dist_min[m_all] = grand_dist_min.get(m_all, 0) + 1
+                if m_all >= 7:
+                    all_ge_7_n += 1
+                worst_consec_min = max(min(cyc[i], cyc[(i+1) % 5])
+                                       for i in range(5))
+                grand_dist_consec[worst_consec_min] = (
+                    grand_dist_consec.get(worst_consec_min, 0) + 1)
+                for i in range(5):
+                    triples_n += 1
+                    n_i = cyc[(i + 1) % 5]
+                    n_ip1 = cyc[(i + 2) % 5]
+                    if n_i >= 7 and n_ip1 >= 7:
+                        bad_triples_n += 1
+                        if len(grand_examples) < 5:
+                            grand_examples.append({
+                                'n_G': n, 'tri_idx': tri_idx, 'v': v, 'i': i,
+                                'cyclic_degs': cyc, 'n_i': n_i, 'n_ip1': n_ip1,
+                                'graph6': G.canonical_label().graph6_string(),
+                            })
+        elapsed = time.time() - start
+        print(f"n={n}: {pairs_n} (G,v) pairs, {triples_n} (G,v,i) triples; "
+              f"{bad_triples_n} triples with both flank-adj deg ≥ 7 "
+              f"[{elapsed:.0f}s]")
+        sys.stdout.flush()
+        grand_pairs += pairs_n
+        grand_triples += triples_n
+        grand_bad_triples += bad_triples_n
+        grand_all_ge_7 += all_ge_7_n
+
+    print()
+    print("=" * 70)
+    print(f"Grand totals across n_G in [12, {max_n}]:")
+    print(f"  (G, v) pairs:                 {grand_pairs}")
+    print(f"  (G, v, i) triples:            {grand_triples}")
+    pct = 100 * grand_all_ge_7 / max(grand_pairs, 1)
+    print(f"  pairs with all 5 neighbours deg ≥ 7: "
+          f"{grand_all_ge_7} ({pct:.2f}%)")
+    pct = 100 * grand_bad_triples / max(grand_triples, 1)
+    print(f"  triples with BOTH flank-adj deg ≥ 7: "
+          f"{grand_bad_triples} ({pct:.2f}%)")
+    print()
+    print("  Distribution of min(all 5 neighbour degs) per (G, v):")
+    for m in sorted(grand_dist_min):
+        c = grand_dist_min[m]
+        ppct = 100 * c / max(grand_pairs, 1)
+        bar = '#' * max(1, int(ppct))
+        print(f"    {m}: {c:>6} ({ppct:5.2f}%) {bar[:50]}")
+    print()
+    print("  Distribution of MAX over i of "
+          "min(n_i, n_{i+1}) per (G, v)\n"
+          "  (i.e., the worst-case consecutive-pair-min --- if this is\n"
+          "  ≤ 6, every i has min(n_i, n_{i+1}) ≤ 6 and the partial proof\n"
+          "  applies; if it is ≥ 7, at least one i has both flanks ≥ 7):")
+    for m in sorted(grand_dist_consec):
+        c = grand_dist_consec[m]
+        ppct = 100 * c / max(grand_pairs, 1)
+        bar = '#' * max(1, int(ppct))
+        print(f"    {m}: {c:>6} ({ppct:5.2f}%) {bar[:50]}")
+    if grand_examples:
+        print()
+        print("  Sample (G, v, i) triples where BOTH flank-adj deg ≥ 7:")
+        for ex in grand_examples:
+            print(f"    n={ex['n_G']}, tri#{ex['tri_idx']}, v={ex['v']}, "
+                  f"i={ex['i']}, "
+                  f"cyclic degs around v = {ex['cyclic_degs']}, "
+                  f"(n_i, n_{{i+1}}) = ({ex['n_i']}, {ex['n_ip1']})")
+            print(f"      graph6: {ex['graph6']}")
+
+
+if __name__ == '__main__':
+    main()