face_monochromatic_pairs: retract n_i = 6 lemma as empirically false

CRITICAL AUDIT FINDING: experiments/check_subcase_iib.py shows that
Lemma (Flank covering, n_i = 6) is empirically FALSE in full
generality, not just unproven:

  Across 142,812 chord-apex+Kempe colourings up to |V(G)| ≤ 20:
    -   9,228 (6.46%) reach sub-case (ii.B) of Case (b)
        (φ(A_i P_1) = c_1 AND φ(P_1 P_2) = c_0);
    -   1,314 (0.92%) of those have P_1 ∉ V(K_b) ∪ V(K_c),
        falsifying the lemma's conclusion ∂F_flank^♭ ⊆ V(K_b) ∪ V(K_c).

So the original n_i = 6 lemma cannot be saved by patching the proof;
the conclusion itself is wrong.

Paper changes:
  - Lemma (Flank covering, n_i = 6): retracted in full generality.
    Restated with a weakened conclusion (true only for Case (a) and
    Case (b) sub-case (i)), with explicit acknowledgement that the
    sub-case (b)(ii) configuration falsifies the lemma on 1,314
    colourings.
  - Proof of the lemma: rewritten to honestly stop at the proven sub-
    cases; sub-case (b)(ii) is identified as unprovable by local
    argument (and now demonstrated empirically false).
  - Theorem (Partial proof via flank): restricted from n_i ∈ {5, 6}
    to n_i = 5 only.
  - Theorem (Extended partial proof): cases relabelled (a'), (b'), (c)
    with a' = (n_i = 5), b' = (n_{i+1} = 5), c = (n_{i+2} = n_{i+4} = 5).
  - Empirical coverage remark: structural proof covers
    7,531 / 7,930 (94.97%) of (G, v, i) configurations up to
    |V(G)| ≤ 20. The other 399 (5.03%) have at least one n_k = 6 but
    no n_k = 5 in the right position; the flank face on the n_k = 6
    side is the natural candidate but is no longer a tight covering.
  - Deciding-face conjecture itself remains empirically true on all
    142,812 colourings; the proof's structural step is what's open
    on the 399 triples.

Lessons from the audit:
  - The "+P_2 ∈ V(K_b) ∪ V(K_c) implies P_1 ∈ V(K_b) ∪ V(K_c)"
    propagation in the original n_i = 6 proof was wrong: the cycle
    type (K_b vs K_c) matters in a way the proof glossed over, and
    specifically when φ(P_1 P_2) = c_0 the K_c cycle through P_2
    doesn't use that edge.
  - A correct n_i = 6 lemma would require a global K_b-walk argument
    showing the {c, c_0}-cycle through P_2 coincides with K_b in the
    bad sub-case. Empirically this is FALSE in 0.92% of colourings,
    so no such argument exists; the n_i = 6 covering must instead come
    from a different face entirely for those colourings.

Paper stays at 21 pages.

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

papers/face_monochromatic_pairs/experiments/check_subcase_iib.py

@@ -0,0 +1,215 @@
+"""Check whether sub-case (ii.B) of Case (b) of the Flank-covering
+lemma (n_i = 6) ever arises in chord-apex+Kempe colourings.
+
+Sub-case (ii.B) is the configuration in which the structural
+propagation argument in the partial proof has a real gap:
+
+  - n_i = 6: F_flank_{i, i+1}^♭ has 2 intermediates P_1, P_2 on the
+    F-arc from A_i to A_{i+1}.
+  - Case (b): varphi(A_i P_1) = c_1.
+  - Sub-case (ii): varphi(P_1 P_2) = c_0.
+  - Derived: varphi(A_{i+1} P_2) = c_1, varphi(P_2 O_2) = c,
+    varphi(P_1 O_1) = c, varphi(A_i Q) = c.
+
+In this sub-case the lemma's local argument (that the cycle at P_2
+passes from P_2 to P_1) needs P_2 ∈ V(K_b), which isn't forced from
+the local data: the {c, c_0}-Kempe cycle through P_2 might not be K_b.
+
+We check: across all chord-apex+Kempe colourings of all reduced duals
+with |V(G)| ≤ 20, does sub-case (ii.B) ever occur? If yes, in how many
+of those configurations is P_1 actually in V(K_b) ∪ V(K_c) (i.e., the
+conclusion of the lemma still holds even though our proof gap is
+real)?
+
+Run with: sage experiments/check_subcase_iib.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 find_flank_arc_intermediates(H, named, i, side):
+    """Return the ordered F-arc from A_i (or A_{i+1}) along F's
+    boundary as a list of vertices.
+
+    side='lower': arc from A_i to A_{i+1} (= F_flank_{i, i+1}^♭).
+    side='upper': arc from A_{i+1} to A_{i+2} (= F_flank_{i+1, i+2}^♭).
+
+    We use the planar embedding of H to walk around the
+    face containing v_n + side_0 + spike (lower) or v_n + spike + side_1
+    (upper).
+    """
+    H.is_planar(set_embedding=True)
+    spike = named['spike']  # frozenset({A_{i+1}, v_n})
+    side_0 = named['side_0']
+    side_1 = named['side_1']
+    # The flank face contains v_n + spike + side_0/side_1 + the arc edges
+    target_edges = set()
+    if side == 'lower':
+        target_edges = {side_0, spike}
+    else:
+        target_edges = {side_1, spike}
+    for face in H.faces():
+        # face is list of (u, v) edges (or tuples of vertex pairs)
+        face_edges_set = {frozenset(e) for e in face}
+        if target_edges.issubset(face_edges_set):
+            # Trace the boundary, return the vertices in cyclic order
+            verts = []
+            for e in face:
+                verts.append(e[0])
+            return verts
+    return None
+
+
+def test_one(D):
+    D.is_planar(set_embedding=True)
+    n_col = 0
+    n_subcase_iib = 0
+    n_subcase_iib_p1_covered = 0  # of those, how many have P_1 ∈ V(K_b) ∪ V(K_c)
+    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
+                # We need to identify P_1, P_2, A_i, A_{i+1}, etc.
+                # Recover the named vertices from `named`.
+                v_n = 9999
+                # named['side_0'] = {A_i, v_n}, named['spike'] = {A_{i+1}, v_n}
+                # side_1 = {A_{i+2}, v_n}, merged = {A_{i+3}, A_{i+4}}
+                A_i = next(iter(named['side_0'] - {v_n}))
+                A_ip1 = next(iter(named['spike'] - {v_n}))
+                A_ip2 = next(iter(named['side_1'] - {v_n}))
+                A_ip3, A_ip4 = sorted(named['merged'])
+                # Get flank arc for lower (A_i → A_{i+1})
+                # The face F_flank_{i, i+1}^♭ has boundary v_n - A_i - ... - A_{i+1} - v_n
+                # Find this face:
+                target_edges = {named['side_0'], named['spike']}
+                arc_verts = None
+                for f in H.faces():
+                    f_edges = {frozenset(e) for e in f}
+                    if target_edges.issubset(f_edges):
+                        arc_verts = [e[0] for e in f]
+                        break
+                if arc_verts is None or len(arc_verts) != 5:
+                    # Not the n_i = 6 case (length 5 flank face)
+                    continue
+                # Identify P_1, P_2 along the arc
+                # The cycle visits v_n, A_i, P_1, P_2, A_{i+1} in some order
+                # (possibly reversed). Find the index of v_n.
+                if v_n not in arc_verts: continue
+                k = arc_verts.index(v_n)
+                cyc = arc_verts[k:] + arc_verts[:k]   # rotate so v_n is first
+                # cyc should be [v_n, A_i, P_1, P_2, A_{i+1}] or
+                # [v_n, A_{i+1}, P_2, P_1, A_i]
+                if cyc[1] == A_i:
+                    P_1, P_2 = cyc[2], cyc[3]
+                    assert cyc[4] == A_ip1
+                elif cyc[1] == A_ip1:
+                    P_2, P_1 = cyc[2], cyc[3]
+                    assert cyc[4] == A_i
+                else:
+                    continue
+                # Check sub-case (ii.B): φ(A_i P_1) = c_1, φ(P_1 P_2) = c_0
+                # c = color of merged/spike
+                merged_idx = edge_idx(edges, named['merged'])
+                c = col[merged_idx]
+                # side_0 has color c_0
+                side_0_idx = edge_idx(edges, named['side_0'])
+                c_0 = col[side_0_idx]
+                # side_1 has color c_1
+                side_1_idx = edge_idx(edges, named['side_1'])
+                c_1 = col[side_1_idx]
+                # Get edge colours of (A_i, P_1) and (P_1, P_2)
+                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 or col[e_P1P2] != c_0:
+                    continue
+                # Sub-case (ii.B) detected
+                n_subcase_iib += 1
+                # Check if P_1 ∈ V(K_b) ∪ V(K_c)
+                a = c
+                other = [x for x in range(3) if x != a]
+                # K_b = {a, b_color} Kempe cycle through merged
+                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)
+                if P_1 in V_b or P_1 in V_c:
+                    n_subcase_iib_p1_covered += 1
+    return n_col, n_subcase_iib, n_subcase_iib_p1_covered
+
+
+def main(max_n=20, time_budget_per_n=1800):
+    print("Check: how often does sub-case (ii.B) of Case (b) of\n"
+          "Lemma 'Flank covering, n_i = 6' actually arise?\n"
+          f"n_G in [12, {max_n}]\n")
+    grand_col = 0
+    grand_sub = 0
+    grand_sub_covered = 0
+    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_col_n = 0; n_sub_n = 0; n_cov_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
+            G.is_planar(set_embedding=True)
+            D = dual_of(G)
+            ni, ns, ncov = test_one(D)
+            n_col_n += ni; n_sub_n += ns; n_cov_n += ncov
+        elapsed = time.time() - start
+        print(f"n={n}: {n_col_n} col., {n_sub_n} sub-case (ii.B) "
+              f"({100*n_sub_n/max(n_col_n, 1):.2f}% of col.); "
+              f"{n_cov_n} of those have P_1 ∈ V(K_b)∪V(K_c) "
+              f"[{elapsed:.0f}s]")
+        sys.stdout.flush()
+        grand_col += n_col_n
+        grand_sub += n_sub_n
+        grand_sub_covered += n_cov_n
+    print()
+    print("=" * 70)
+    print(f"Grand totals: {grand_col} chord-apex+Kempe colourings")
+    print(f"  sub-case (ii.B) detected: {grand_sub} "
+          f"({100*grand_sub/max(grand_col, 1):.2f}%)")
+    if grand_sub > 0:
+        print(f"  of those, P_1 ∈ V(K_b)∪V(K_c): {grand_sub_covered} "
+              f"({100*grand_sub_covered/max(grand_sub, 1):.2f}%)")
+        gap_open = grand_sub - grand_sub_covered
+        print(f"  of those, P_1 NOT in V(K_b)∪V(K_c): {gap_open}")
+    else:
+        print("  Sub-case (ii.B) never arises empirically.")
+        print("  → the proof gap is structurally INACTIVE")
+        print("  → the n_i = 6 lemma's conclusion is empirically tight")
+
+
+if __name__ == '__main__':
+    main()