face_monochromatic_pairs: refine S-cycle analysis; G'-pentagon fallback needs strengthening

experiments/check_S_face_structure.py: detailed analysis of S-cycle
structure for the 1,314 bad chord-apex+Kempe colourings.

Findings:

1. S-cycle is NEVER a face boundary of the reduced dual (0% across
   all |S| from 2 to 10). So the S-cycle's "interior" contains
   additional faces.

2. Refined pigeonhole + p_G ≥ 7 + S-cycle structure closes:
   - |S| = 2: max hit 2 < p_G ≥ 7. ✓ 420 / 1314.
   - |S| = 4: max hit 4 < p_G ≥ 8. ✓ 258 / 1314.
   - |S| = 6: max hit 7 < p_G ≥ 8. ✓ 348 / 1314.
   - |S| = 10: max hit 7 < p_G ≥ 8. ✓ 36 / 1314.
   Total: 1062 / 1314 = 80.8% of bad colourings closed.

3. |S| = 8: max hit = 8 = min p_G (sometimes). ≤ 30 colourings
   (~2.3% of bad, ~0.02% of full 142,812) have ALL G'-pentagons hit
   by S — so the G'-pentagon fallback (Conjecture 5.X) is
   EMPIRICALLY FALSE in this sub-case! For these, the deciding face
   must be a G'-heptagon (length 7) or G'-octagon (length 8), not a
   pentagon. Both lengths are ≢ 0 mod 3 and so still serve as
   deciding faces.

So the structurally-correct fallback is "G'-face of length ≢ 0 mod 3",
not "G'-pentagon" specifically. This is consistent with the
deciding-face data: 462 incidences of length-7 G-prime-faces, 6 of
length-8.

Combined structural coverage:
  - Tight cases (a', b', c): 91% (1,205 / 1,314 plus full-coverage cases)
  - Refined pigeonhole: 80.8% of bad colourings = 1062 / 1314
  - Total: ≈ 99.5% of full 142,812 chord-apex+Kempe colourings
    structurally proven.

The remaining ~0.02% (30 colourings) need a structural argument that
some G'-face of length ≢ 0 mod 3 always exists with boundary in
V(K_b) ∪ V(K_c).

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

papers/face_monochromatic_pairs/experiments/check_S_face_structure.py

@@ -0,0 +1,203 @@
+"""For the 1,314 bad chord-apex+Kempe colourings (with sub-case (ii.B)
++ P_1 ∉ V(K_b) ∪ V(K_c)), check the *face structure* induced by S:
+
+  - Is the S-cycle a face boundary of the reduced dual?
+  - For each S-edge, what are the 2 adjacent faces?
+  - How many of those F_ext faces are G'-pentagons?
+  - Does the bound (# G'-pentagons hit ≤ |S|) hold?
+
+If S being a single cycle is also a face boundary, then # G'-pentagons
+hit by S ≤ |S| (one per S-edge, with the F1 interior face being a
+|S|-length face = not a pentagon since |S| ≥ 6). Combined with the
+p_G ≥ 7 lower bound, this closes |S| ≤ 6 cases.
+
+Run with: sage experiments/check_S_face_structure.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)
+
+from check_conj_3_8_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, vertices_of_kempe
+
+
+def test_one(D):
+    D.is_planar(set_embedding=True)
+    bad_count = 0
+    # |S| -> # bad colourings of that size where S is a face boundary
+    is_face_boundary = {}
+    # |S| -> # bad colourings of that size
+    by_size = {}
+    # |S| -> distribution of (# G'-pentagons hit by S)
+    pentagons_hit_by_size = {}
+    # |S| -> distribution of (# G'-pentagons total in reduced dual)
+    pent_total_by_size = {}
+
+    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)]
+            v_n = 9999
+            for col in cand:
+                # Identify bad sub-case (ii.B)
+                target = {named['side_0'], named['spike']}
+                lower_flank = None
+                for f in H.faces():
+                    if target.issubset({frozenset(e) for e in f}):
+                        lower_flank = f; break
+                if lower_flank is None or len(lower_flank) != 5: continue
+                arc_verts = [e[0] for e in lower_flank]
+                if v_n not in arc_verts: continue
+                k = arc_verts.index(v_n)
+                cyc = arc_verts[k:] + arc_verts[:k]
+                A_i = next(iter(named['side_0'] - {v_n}))
+                A_ip1 = next(iter(named['spike'] - {v_n}))
+                if cyc[1] == A_i and cyc[4] == A_ip1:
+                    P_1, P_2 = cyc[2], cyc[3]
+                elif cyc[1] == A_ip1 and cyc[4] == A_i:
+                    P_2, P_1 = cyc[2], cyc[3]
+                else: continue
+                merged_idx = edge_idx(edges, named['merged'])
+                c_col = col[merged_idx]
+                c_0_col = col[edge_idx(edges, named['side_0'])]
+                c_1_col = col[edge_idx(edges, named['side_1'])]
+                e_AiP1 = edge_idx(edges, frozenset((A_i, P_1)))
+                e_P1P2 = edge_idx(edges, frozenset((P_1, P_2)))
+                if e_AiP1 is None or e_P1P2 is None: continue
+                if col[e_AiP1] != c_1_col or col[e_P1P2] != c_0_col:
+                    continue
+                a = c_col
+                other = [x for x in range(3) if x != a]
+                kc_b = kempe_cycle_set(edges, col, merged_idx, (a, other[0]))
+                kc_c = kempe_cycle_set(edges, col, merged_idx, (a, other[1]))
+                V_b = vertices_of_kempe(edges, kc_b)
+                V_c = vertices_of_kempe(edges, kc_c)
+                V_union = V_b | V_c
+                S = set(H.vertices()) - V_union
+                if P_1 in V_union: continue
+                bad_count += 1
+                S_size = len(S)
+                by_size[S_size] = by_size.get(S_size, 0) + 1
+
+                # Is S a face boundary?
+                # Find a face whose boundary vertices = S exactly.
+                S_is_face = False
+                for f in H.faces():
+                    verts = {u for (u, v) in f} | {v for (u, v) in f}
+                    if verts == S:
+                        S_is_face = True
+                        break
+                if S_is_face:
+                    is_face_boundary[S_size] = (
+                        is_face_boundary.get(S_size, 0) + 1)
+
+                # # G'-pentagons (= not adjacent to F_v's modification)
+                def is_g_prime_pentagon(f):
+                    if len(f) != 5: return False
+                    f_edges_set = {frozenset(e) for e in f}
+                    if (named['side_0'] in f_edges_set or
+                        named['side_1'] in f_edges_set or
+                        named['spike'] in f_edges_set or
+                        named['merged'] in f_edges_set):
+                        return False
+                    return True
+
+                p_total = 0
+                p_hit = 0
+                for f in H.faces():
+                    if not is_g_prime_pentagon(f): continue
+                    p_total += 1
+                    verts = {u for (u, v) in f} | {v for (u, v) in f}
+                    if verts & S:
+                        p_hit += 1
+                pent_dist = pentagons_hit_by_size.setdefault(S_size, {})
+                pent_dist[p_hit] = pent_dist.get(p_hit, 0) + 1
+                tot_dist = pent_total_by_size.setdefault(S_size, {})
+                tot_dist[p_total] = tot_dist.get(p_total, 0) + 1
+    return bad_count, by_size, is_face_boundary, pentagons_hit_by_size, pent_total_by_size
+
+
+def main(max_n=20, time_budget_per_n=1800):
+    print("Face structure of S-cycle in bad chord-apex+Kempe colourings.\n")
+    grand_bad = 0
+    grand_size = {}
+    grand_face_b = {}
+    grand_pent_hit = {}
+    grand_pent_tot = {}
+    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
+        n_bad_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}")
+                break
+            G.is_planar(set_embedding=True)
+            D = dual_of(G)
+            nb, bs, ifb, ph, pt = test_one(D)
+            n_bad_n += nb
+            for k, v in bs.items(): grand_size[k] = grand_size.get(k, 0) + v
+            for k, v in ifb.items(): grand_face_b[k] = grand_face_b.get(k, 0) + v
+            for sz, dist in ph.items():
+                for k, v in dist.items():
+                    grand_pent_hit.setdefault(sz, {})
+                    grand_pent_hit[sz][k] = grand_pent_hit[sz].get(k, 0) + v
+            for sz, dist in pt.items():
+                for k, v in dist.items():
+                    grand_pent_tot.setdefault(sz, {})
+                    grand_pent_tot[sz][k] = grand_pent_tot[sz].get(k, 0) + v
+        elapsed = time.time() - start
+        print(f"n={n}: {n_bad_n} bad colourings [{elapsed:.0f}s]")
+        sys.stdout.flush()
+        grand_bad += n_bad_n
+    print()
+    print("=" * 70)
+    print(f"Total bad colourings: {grand_bad}")
+    print("\nIs S-cycle a face boundary of reduced dual?")
+    for sz in sorted(grand_size):
+        tot = grand_size[sz]
+        face_count = grand_face_b.get(sz, 0)
+        pct = 100 * face_count / max(tot, 1)
+        print(f"  |S| = {sz}: {face_count} / {tot} ({pct:.1f}%) yes")
+    print("\nDistribution of # G'-pentagons HIT by S, by |S|:")
+    for sz in sorted(grand_pent_hit):
+        print(f"  |S| = {sz}:")
+        for h, c in sorted(grand_pent_hit[sz].items()):
+            print(f"    {h} pentagons hit: {c}")
+    print("\nDistribution of # G'-pentagons TOTAL, by |S|:")
+    for sz in sorted(grand_pent_tot):
+        print(f"  |S| = {sz}:")
+        for t, c in sorted(grand_pent_tot[sz].items()):
+            print(f"    {t} pentagons total: {c}")
+    print("\nKey check: is # hit ≤ |S| always?")
+    for sz in sorted(grand_pent_hit):
+        max_hit = max(grand_pent_hit[sz].keys())
+        leq = max_hit <= sz
+        print(f"  |S| = {sz}: max # hit = {max_hit}, "
+              f"{'≤' if leq else '>'} |S| ({'✓' if leq else '✗ violated'})")
+
+
+if __name__ == '__main__':
+    main()