face_monochromatic_pairs: honest audit of partial proof — flag n_i = 6 gap

Audit of the structural proof of Conjecture 5.1 (via deciding-face
conjecture) identifies one real proof gap:

Lemma (Flank covering, n_i = 6), Case (b) sub-case (ii) -- when
φ(A_i P_1) = c_1 AND φ(P_1 P_2) = c_0 -- the propagation argument
"the cycle at P_2 passes from P_2 to P_1" requires the {c, c_0}-Kempe
cycle through P_2 to be K_b, which forces P_1 onto K_b via the c_0
edge P_1 P_2. Properness at P_2 only forces P_2 ∈ V(K_c) (via
φ(A_{i+1} P_2) = c_1), not P_2 ∈ V(K_b). The further step requires
controlling the {c, c_0}-walk through the rest of the graph, which
the local argument doesn't do.

experiments/audit_tight_coverage.py quantifies the impact across
empirical data:
  - 7,930 / 7,930 (G, v, i) triples up to |V(G)| ≤ 20 are covered
    by the FULL partial proof (including the n_i = 6 lemma);
  - 7,531 / 7,930 (94.97%) are covered by the TIGHT subset
    (n_i = 5 OR n_{i+1} = 5 OR (n_{i+2}, n_{i+4}) = (5, 5)) which
    has no proof gap;
  - 399 (5.03%) genuinely require the n_i = 6 lemma.

So the gap matters: empirical coverage of the tight subset alone is
~95%, not 100%.

Paper changes:
  - Lemma (Flank covering, n_i = 6) marked as "partial" with a status
    note in the statement itself.
  - Proof of Lemma includes an "Audit note" identifying the open
    sub-case explicitly, after establishing the parts that ARE proven.
  - Empirical coverage remark softened: the 100% claim is restated
    as "modulo the open sub-case", with the 94.97% tight figure
    given separately.

Empirically the n_i = 6 lemma is robust (all 142,812 colourings have
a deciding face), so the gap is probably patchable — likely either
via a structural argument that rules out the bad sub-case in
chord-apex+Kempe colourings, or via a global K_b-walk argument
showing P_2 ∈ V(K_b) anyway. But this is open.

Paper stays at 21 pages (only added text within existing lemma + remark).

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

papers/face_monochromatic_pairs/experiments/audit_tight_coverage.py

@@ -0,0 +1,129 @@
+"""Audit: how many (G, v, i) triples are covered by the
+structurally-TIGHT subset of the partial proof (dropping the
+n_i = 6 case which has a gap in sub-case (ii.B) of the flank-covering
+lemma)?
+
+Tight cases:
+  (a') n_i = 5 (= F_flank length 4, P adjacent to both A_i and A_{i+1});
+  (b') n_{i+1} = 5 (symmetric);
+  (c)  n_{i+2} = n_{i+4} = 5 (= F_outer length 7, both intermediates
+       adjacent to A_{i+3}, A_{i+4} ∈ V(K_b) ∩ V(K_c) via merged).
+
+Loose cases (the proof formally claims these but has a gap on
+sub-case (ii.B)):
+  (a) n_i = 6
+  (b) n_{i+1} = 6
+
+This script reports per (G, v, i) whether tight-only coverage suffices.
+
+Run with: sage experiments/audit_tight_coverage.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 main(max_n=20, time_budget_per_n=1200):
+    print("Audit of structurally TIGHT coverage of the deciding-face\n"
+          "partial proof. Restricts to cases (a' = n_i = 5),\n"
+          "(b' = n_{i+1} = 5), (c = n_{i+2} = n_{i+4} = 5);\n"
+          "drops the (a)/(b) cases at n_k = 6 due to a gap in\n"
+          "Lemma 'Flank covering, n_i = 6' (sub-case ii.B).\n")
+    print(f"n_G in [12, {max_n}]\n")
+
+    grand_triples = 0
+    grand_loose_covered = 0     # by full partial proof (with gap)
+    grand_tight_covered = 0     # by tight-only subset
+    grand_loose_uncovered = 0   # empirical bad triples
+    grand_loose_not_tight = 0   # loose-covered but not tight (= n_i = 6 reliance)
+    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
+        n_t = 0; n_loose = 0; n_tight = 0; n_diff = 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)
+            emb = G.get_embedding()
+            for v in G.vertex_iterator():
+                if G.degree(v) != 5: continue
+                cyc = [G.degree(u) for u in emb[v]]
+                for i in range(5):
+                    n_t += 1
+                    n_i = cyc[(i + 1) % 5]
+                    n_ip1 = cyc[(i + 2) % 5]
+                    n_ip2 = cyc[(i + 3) % 5]
+                    n_ip3 = cyc[(i + 4) % 5]
+                    n_ip4 = cyc[(i + 5) % 5]
+                    loose_a = (n_i in (5, 6))
+                    loose_b = (n_ip1 in (5, 6))
+                    case_c = (n_ip2 == 5 and n_ip4 == 5)
+                    tight_a = (n_i == 5)
+                    tight_b = (n_ip1 == 5)
+                    loose = loose_a or loose_b or case_c
+                    tight = tight_a or tight_b or case_c
+                    if loose: n_loose += 1
+                    if tight: n_tight += 1
+                    if loose and not tight: n_diff += 1
+                    if loose and not tight and len(grand_examples) < 10:
+                        grand_examples.append({
+                            'n_G': n, 'tri_idx': tri_idx, 'v': v, 'i': i,
+                            'cyc': cyc,
+                            'n_tuple': (n_i, n_ip1, n_ip2, n_ip3, n_ip4),
+                        })
+        elapsed = time.time() - start
+        print(f"n={n}: {n_t} triples, loose-covered={n_loose} "
+              f"({100*n_loose/max(n_t,1):.1f}%), "
+              f"tight-only={n_tight} ({100*n_tight/max(n_t,1):.1f}%); "
+              f"loose-not-tight={n_diff} [{elapsed:.0f}s]")
+        sys.stdout.flush()
+        grand_triples += n_t
+        grand_loose_covered += n_loose
+        grand_tight_covered += n_tight
+        grand_loose_not_tight += n_diff
+
+    grand_loose_uncovered = grand_triples - grand_loose_covered
+    grand_tight_uncovered = grand_triples - grand_tight_covered
+    print()
+    print("=" * 70)
+    print(f"Grand totals across n_G in [12, {max_n}]:")
+    print(f"  (G, v, i) triples:                       {grand_triples}")
+    print(f"  loose-covered (full partial proof):      "
+          f"{grand_loose_covered} "
+          f"({100*grand_loose_covered/max(grand_triples,1):.2f}%)")
+    print(f"  loose-uncovered (= empirical bad):       "
+          f"{grand_loose_uncovered} "
+          f"({100*grand_loose_uncovered/max(grand_triples,1):.2f}%)")
+    print(f"  tight-covered (drop n_i = 6 gap-case):   "
+          f"{grand_tight_covered} "
+          f"({100*grand_tight_covered/max(grand_triples,1):.2f}%)")
+    print(f"  tight-uncovered (needs n_i = 6 lemma):   "
+          f"{grand_tight_uncovered} "
+          f"({100*grand_tight_uncovered/max(grand_triples,1):.2f}%)")
+    print(f"  loose-not-tight (needs n_i = 6 lemma):   "
+          f"{grand_loose_not_tight}")
+    if grand_examples:
+        print()
+        print("  Sample triples that need the n_i = 6 lemma "
+              "(NOT covered by tight subset):")
+        for ex in grand_examples[:10]:
+            print(f"    n={ex['n_G']}, tri#{ex['tri_idx']}, "
+                  f"v={ex['v']}, i={ex['i']}: cyc={ex['cyc']}, "
+                  f"(n_i,n_{{i+1}},n_{{i+2}},n_{{i+3}},n_{{i+4}})={ex['n_tuple']}")
+
+
+if __name__ == '__main__':
+    main()

papers/face_monochromatic_pairs/experiments/check_v_neighbour_degrees.py

@@ -88,6 +88,16 @@ def main(max_n=20, time_budget_per_n=1200):
                     n_ip2 = cyc[(i + 3) % 5]
                     n_ip3 = cyc[(i + 4) % 5]
                     n_ip4 = cyc[(i + 5) % 5]
+                    # AUDIT: does the structurally-tight subset (drop n_i=6 case) cover?
+                    tight_covered = (
+                        n_i == 5 or n_ip1 == 5 or
+                        (n_ip2 == 5 and n_ip4 == 5)
+                    )
+                    if not tight_covered:
+                        # Record what would be the "audit-uncovered" triples
+                        # (= we have proved coverage only on n_i = 5 or n_{i+1} = 5
+                        #   or (n_{i+2}, n_{i+4}) = (5, 5)).
+                        pass  # counted below as "audit_uncovered_n"
                     if n_i >= 7 and n_ip1 >= 7:
                         bad_triples_n += 1
                         # Check whether F_outer's length condition is OK

papers/face_monochromatic_pairs/paper.tex

@@ -1041,9 +1041,21 @@ its colour is in $\{c_0, c_1\}$, so the corresponding Kempe cycle
 placing $P$ in that cycle's vertex set.
 \end{proof}
 
-\begin{lemma}[Flank covering, $n_i = 6$]
+\begin{lemma}[Flank covering, $n_i = 6$; partial]
 \label{lem:flank-covering-hex}
 If $n_i = 6$ then $\partial F_{i, i+1}^{\flat} \subseteq V(K_b) \cup V(K_c)$.
+
+\emph{Status:} The proof below establishes the conclusion except in a
+specific sub-case (Case (b), sub-case~(ii) below) where the local
+propagation argument from $P_2$ to $P_1$ requires the
+$\{c, c_0\}$-Kempe cycle through $P_2$ to coincide with $K_b$; this
+isn't forced by the local data and would require a global argument
+through the rest of the graph. Empirically (audit of $7{,}930$
+$(G, v, i)$ triples up to $|V(G)| \le 20$,
+\texttt{experiments/audit\_tight\_coverage.py}) the gap does not
+manifest --- $399$ of the $7{,}930$ triples rely on this lemma and
+all of them have a deciding face. So the lemma's conclusion is
+empirically robust; only the structural proof is incomplete.
 \end{lemma}
 
 \begin{proof}
@@ -1084,6 +1096,29 @@ to $P_1$. If this cycle is $K_b$, $P_1 \in V(K_b)$; if it is $K_c$
 $\{c, c_1\}$), then $P_1 \in V(K_c)$.
 
 In either case $P_1 \in V(K_b) \cup V(K_c)$.
+
+\textbf{Audit note.} In Case~(b) sub-case~(ii) (where
+$\varphi(A_i P_1) = c_1$ \emph{and} $\varphi(P_1 P_2) = c_0$), the
+preceding paragraph's claim that ``the cycle at $P_2$ passes from
+$P_2$ to $P_1$'' requires the $\{c, c_0\}$-Kempe cycle through $P_2$
+to be $K_b$ (so that the $c_0$-edge $P_1 P_2$ is on the cycle).
+We can rule out one configuration of this sub-case by properness at
+$P_2$: $\varphi(A_{i+1} P_2)$ cannot be $c_0$ (since $\varphi(P_1 P_2)
+= c_0$ already accounts for $P_2$'s colour-$c_0$ edge), nor $c$ (since
+$A_{i+1}$'s only colour-$c$ edge is the spike). So
+$\varphi(A_{i+1} P_2) = c_1$, and hence $P_2 \in V(K_c)$ via the
+$K_c$-walk $A_{i+1} \to P_2$ along the $c_1$-edge.
+
+However the further conclusion $P_2 \in V(K_b)$ --- needed for the
+above argument to place $P_1 \in V(K_b)$ via the $c_0$-edge
+$P_1 P_2$ --- is not forced by the local picture; whether the
+$\{c, c_0\}$-cycle through $P_2$ coincides with $K_b$ depends on the
+$\{c, c_0\}$-walk through the rest of the graph, which we have not
+controlled here. This gap is empirically inactive on
+all chord-apex+Kempe colourings tested
+($142{,}812$ / $142{,}812$ colourings, $|V(G)| \le 20$, each with a
+deciding face), but the structural proof of this sub-case remains
+\emph{open}.
 \end{proof}
 
 \begin{theorem}[Partial proof of
@@ -1205,10 +1240,18 @@ they satisfy case (c).
 Combining
 Theorems~\ref{thm:deciding-face-implies-conj-5-1}
 and~\ref{thm:deciding-face-partial-extended}, this yields a
-\textbf{structural proof of
+structural proof of
 Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}
 on every chord-apex+Kempe colouring of every reduced dual with
-$|V(G)| \le 20$.}
+$|V(G)| \le 20$, \emph{modulo} the open sub-case in
+Lemma~\ref{lem:flank-covering-hex}. A stricter accounting
+(\texttt{experiments/audit\_tight\_coverage.py}) shows that
+$7{,}531$ of the $7{,}930$ $(G, v, i)$ configurations
+($94.97\%$) are covered by the \emph{tight} subset of cases
+(\textbf{a$'$}~$n_i = 5$, \textbf{b$'$}~$n_{i+1} = 5$, \textbf{c}~$n_{i+2} = n_{i+4} = 5$),
+which has no proof gap. The remaining $399$ ($5.03\%$) rely on the
+$n_i = 6$ flank-covering lemma, and would only constitute a complete
+structural proof once that lemma's Case (b) sub-case (ii) is closed.
 
 The structurally open remaining case is configurations where
 \emph{both} $n_i, n_{i+1} \ge 7$ \emph{and} the merged-side