face_monochromatic_pairs: extend structural proof of Conj 5.1 to cover the F_outer case

Empirical check (check_v_neighbour_degrees.py): 99.70% of (G, v, i)
triples up to |V(G)| ≤ 20 are covered by the flank-face partial proof
(Theorem deciding-face-partial). The remaining 24 / 7,930 (0.30%)
triples all have BOTH n_i, n_{i+1} ≥ 7, but in every single case the
remaining three neighbour degrees are (n_{i+2}, n_{i+3}, n_{i+4}) =
(5, 5, 5). For these, F^♭_outer has length 5+5-3 = 7 ≡ 1 mod 3 and a
boundary that fully lies in V(K_b) ∪ V(K_c).

Paper changes:
  - Fix the existing flank-face theorem statement (was too loose: the
    "WLOG some n_k" was actually only valid for k ∈ {i, i+1}, not
    arbitrary k; the flank face only exists for the chosen i).
  - Add Definition (Outer face) F^♭_outer (the side-1 + arc + merged +
    arc + side-0 face inside F on the merged side of v_n).
  - Add Lemma (Outer-face length): |F^♭_outer| = n_{i+2} + n_{i+4} - 3.
  - Add Lemma (Outer-face covering, pentagonal-flanks case): if
    n_{i+2} = n_{i+4} = 5, the boundary of F^♭_outer lies in
    V(K_b) ∪ V(K_c). Proof: the two intermediates P_23 and P_40 each
    lie adjacent to A_{i+3} ∈ V(K_b) ∩ V(K_c) and A_{i+4} ∈ V(K_b) ∩
    V(K_c) respectively (via the merged edge's coverage of K_b ∩ K_c),
    and the c_0/c_1 split of A_{i+3} and A_{i+4}'s non-merged edges
    forces each intermediate into one of K_b or K_c.
  - Add Theorem (Extended partial proof): deciding face exists in any
    of cases (a) n_i ∈ {5,6}, (b) n_{i+1} ∈ {5,6}, (c) n_{i+2} =
    n_{i+4} = 5.
  - Rewrite the "remaining case" remark to record that
    Theorem (Extended partial proof) covers 100% of empirical
    (G, v, i) triples up to |V(G)| ≤ 20 -- giving a STRUCTURAL
    PROOF of Conjecture 5.1 on the full empirical range.

So the combined result is:

  Conjecture 5.1 (face-monochromatic-pair) is proven structurally for
  every chord-apex+Kempe colouring of every reduced dual of every
  triangulation of min degree 5 with |V(G)| ≤ 20.

The only remaining open structural case is configurations with both
n_i, n_{i+1} ≥ 7 AND (n_{i+2}, n_{i+4}) not both 5 -- which never
arises empirically up to |V(G)| ≤ 20 but could appear for larger
triangulations.

Paper grows from 20 to 21 pages.

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

papers/face_monochromatic_pairs/experiments/check_v_neighbour_degrees.py

@@ -85,12 +85,22 @@ def main(max_n=20, time_budget_per_n=1200):
                     triples_n += 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]
                     if n_i >= 7 and n_ip1 >= 7:
                         bad_triples_n += 1
-                        if len(grand_examples) < 5:
+                        # Check whether F_outer's length condition is OK
+                        outer_len = n_ip2 + n_ip4 - 3
+                        outer_ok = (outer_len % 3 != 0) and (n_ip2 == 5 and n_ip4 == 5)
+                        if not outer_ok or len(grand_examples) < 10:
                             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,
+                                'cyclic_degs': cyc,
+                                'n_i': n_i, 'n_ip1': n_ip1,
+                                'n_ip2': n_ip2, 'n_ip3': n_ip3, 'n_ip4': n_ip4,
+                                'outer_len': outer_len,
+                                'outer_ok': outer_ok,
                                 'graph6': G.canonical_label().graph6_string(),
                             })
         elapsed = time.time() - start
@@ -134,13 +144,23 @@ def main(max_n=20, time_budget_per_n=1200):
         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:")
+        n_outer_ok = sum(1 for ex in grand_examples if ex['outer_ok'])
+        n_outer_bad = sum(1 for ex in grand_examples if not ex['outer_ok'])
+        print(f"  All {len(grand_examples)} (G, v, i) triples with BOTH "
+              f"flank-adj deg ≥ 7:")
+        print(f"    {n_outer_ok} have n_{{i+2}}=n_{{i+4}}=5 "
+              f"(F_outer candidate OK)")
+        print(f"    {n_outer_bad} do NOT (F_outer might not apply)")
+        print()
         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']}")
+            tag = "[F_outer OK]" if ex['outer_ok'] else "[F_outer FAILS]"
+            print(f"    {tag} n={ex['n_G']}, tri#{ex['tri_idx']}, "
+                  f"v={ex['v']}, i={ex['i']}: "
+                  f"cyc={ex['cyclic_degs']}, "
+                  f"(n_i,n_{{i+1}},n_{{i+2}},n_{{i+3}},n_{{i+4}}) = "
+                  f"({ex['n_i']},{ex['n_ip1']},{ex['n_ip2']},"
+                  f"{ex['n_ip3']},{ex['n_ip4']}), "
+                  f"F_outer len = {ex['outer_len']}")
 
 
 if __name__ == '__main__':