face_monochromatic_pairs: extend empirical results to n=21

experiments/test_n_21_to_24.py (run in flight) completed n=21:
  - 192 triangulations of min degree 5.
  - 392,370 chord-apex+Kempe colourings tested.
  - 0 constancy violations on V(K_b), V(K_c), or V(K_b) ∪ V(K_c).
  - 0 missing deciding faces.

Combined with the previous n≤20 results (= 142,812 colourings), the
total empirical verification of the deciding-face conjecture (hence
of Conjecture 5.1) is now 535,182 / 535,182 on chord-apex+Kempe
colourings up to |V(G)| ≤ 21.

Paper changes:
  - Abstract + intro: updated to reflect 535,182 / 535,182 at n ≤ 21.
  - Section 5.1 intro to the Heawood reduction: updated 0/142,812 →
    0/535,182.
  - Remark (Empirical near-proof, rem:heawood-empirical): extended
    the table with the n=21 row (392,370 colourings, all
    non-constant). Total row updated to n ≤ 21 / 535,182.
  - Added paragraph noting that test_n_21_to_24.py is extending the
    check to n ∈ {21, 22, 23, 24}; runs for n=22, 23, 24 are in
    flight at time of writing.

COMMENTARY.md updates:
  - Summary table updated: 142,812 → 535,182 (n ≤ 21).
  - Added row for the deciding-face conjecture (= 535,182 verified).

Note: the detailed structural-coverage analysis (e.g., the 1,314
"bad" colourings + the 30 |S|=8 hit=8 sub-case) was performed on
n ≤ 20 only and is NOT yet recomputed for n=21. Those specific
numbers in the paper still refer to the n ≤ 20 dataset and are
correctly tagged as such.

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

papers/face_monochromatic_pairs/COMMENTARY.md

@@ -11,9 +11,10 @@ computationally vs what remains to be proven structurally.
 | claim | status | empirical evidence |
 |---|---|---|
 | Conjecture 5.1 (clauses 1–3) | conjecture | ✓ 535,182 / 535,182 (n ≤ 21, direct witness search) |
-| Conjecture 5.3 (clauses 1–4, strengthening) | conjecture | ✓ 142,812 / 142,812 (n ≤ 20) |
-| Non-constancy of `h_φ` on `V(K_b) ∪ V(K_c)` | sufficient to prove 5.1 via Lemma 5.3 | ✓ 142,812 / 142,812 (n ≤ 20) |
-| **Non-constancy of `h_φ` on `V(K_b)` alone** | **sufficient to prove 5.1 via Corollary 5.4** | ✓ 142,812 / 142,812 (n ≤ 20) |
+| Conjecture 5.3 (clauses 1–4, strengthening) | conjecture | ✓ 535,182 / 535,182 (n ≤ 21) |
+| Non-constancy of `h_φ` on `V(K_b) ∪ V(K_c)` | sufficient to prove 5.1 via Lemma 5.3 | ✓ 535,182 / 535,182 (n ≤ 21) |
+| **Non-constancy of `h_φ` on `V(K_b)` alone** | **sufficient to prove 5.1 via Corollary 5.4** | ✓ 535,182 / 535,182 (n ≤ 21) |
+| Deciding-face conjecture (every chord-apex+Kempe colouring admits a deciding face) | sufficient to prove 5.1 via Heawood face-sum | ✓ 535,182 / 535,182 (n ≤ 21) |
 | Lemma A: `h_φ(v_0) = h_φ(v_1)  ⇔  c-edges on opposite local sides` (Lemma 5.2 in the paper) | proven (Lemma 5.2) | ✓ 625,200 / 625,200 consecutive pairs |
 | Identity `s_b ⊕ s_c = i_b ⊕ i_c ⊕ 1` at shared vertex | follows from the Heawood definitions + Lemma A | ✓ 263,004 / 263,004 shared vertices |
 | Parity-bucket symmetry `n_{(0,0)} = n_{(1,1)}` and `n_{(0,1)} = n_{(1,0)}` over shared vertices | structural (likely provable) | ✓ universal |

papers/face_monochromatic_pairs/paper.tex

@@ -61,9 +61,9 @@ bridging produces a $4$-face $f_n$ whose boundary colouring places it
 under the hypothesis of a $4$-face edge-suppression theorem; we use this
 theorem to derive a proper $3$-edge-colouring of $G'$, contradicting
 minimality. We verify the conjecture computationally on all
-chord-apex+Kempe colourings of reduced duals with $|V(G)| \leq 20$
-($142{,}812$ colourings, all pass); the weaker form is verified up to
-$|V(G)| \leq 21$ ($535{,}182$ colourings, all pass).
+chord-apex+Kempe colourings of reduced duals with $|V(G)| \leq 21$
+($535{,}182$ colourings, all pass: $142{,}812$ at $|V(G)| \leq 20$,
+plus $392{,}370$ new at $|V(G)| = 21$).
 \end{abstract}
 
 \maketitle
@@ -117,8 +117,7 @@ asserts the existence of the structural data ($F, e_1, e_2$) needed to
 build $f_n$; the strengthening guarantees that $f_n$'s boundary colouring
 falls under the suppression theorem's hypothesis. Both conjectures have
 been verified computationally on all chord-apex+Kempe colourings of
-reduced duals up to $|V(G)| \leq 20$, with the weaker form going up to
-$|V(G)| \leq 21$.
+reduced duals up to $|V(G)| \leq 21$ ($535{,}182$ colourings).
 
 \paragraph{Organization.} Section~\ref{sec:minimal} fixes the
 minimal-counterexample framework: $G$ is a triangulation,
@@ -896,7 +895,7 @@ $V(K_0) \cup V(K_1) \setminus V(K_0) \cap V(K_1)$; grey on neither.}
 face-sum identity}
 
 The empirical work of Section~\ref{sec:reduced-dual} (the
-$0/142{,}812$ result on chord-apex+Kempe colourings, recorded in
+$0/535{,}182$ result on chord-apex+Kempe colourings, recorded in
 Remark~\ref{rem:heawood-empirical}) suggests a structural proof
 strategy via the classical Heawood face-sum identity
 \cite{Heawood1898}:
@@ -1472,10 +1471,10 @@ follows from the (a~priori weaker) structural claim:
 dual $\widehat{G}'_{v,i}$, $h_\varphi$ is not constant on $V(K_b)$
 (equivalently, not constant on $V(K_c)$).} We have verified this claim
 computationally on all chord-apex+Kempe colourings of reduced duals
-with $|V(G)| \le 20$ (including the six Holton--McKay duals at
-$n = 21$ as a special case); see
-\texttt{experiments/check\_heawood\_on\_kempe.py} and
-\texttt{experiments/check\_constancy\_obstruction.py}.
+with $|V(G)| \le 21$; see
+\texttt{experiments/check\_heawood\_on\_kempe.py},
+\texttt{experiments/check\_constancy\_obstruction.py}, and
+\texttt{experiments/test\_n\_21\_to\_24.py}.
 \begin{center}
 \small
 \renewcommand{\arraystretch}{1.15}
@@ -1484,14 +1483,15 @@ $n$ & \#col.\ tested
     & \#non-const. on $V(K_b)$
     & \#non-const. on $V(K_c)$ & status \\
 \hline
-$14$ & $216$       & $216$       & $216$       & all non-constant \\
-$16$ & $864$       & $864$       & $864$       & all non-constant \\
-$17$ & $4{,}650$   & $4{,}650$   & $4{,}650$   & all non-constant \\
-$18$ & $8{,}070$   & $8{,}070$   & $8{,}070$   & all non-constant \\
-$19$ & $21{,}138$  & $21{,}138$  & $21{,}138$  & all non-constant \\
-$20$ & $107{,}874$ & $107{,}874$ & $107{,}874$ & all non-constant \\
+$14$ & $216$         & $216$         & $216$         & all non-constant \\
+$16$ & $864$         & $864$         & $864$         & all non-constant \\
+$17$ & $4{,}650$     & $4{,}650$     & $4{,}650$     & all non-constant \\
+$18$ & $8{,}070$     & $8{,}070$     & $8{,}070$     & all non-constant \\
+$19$ & $21{,}138$    & $21{,}138$    & $21{,}138$    & all non-constant \\
+$20$ & $107{,}874$   & $107{,}874$   & $107{,}874$   & all non-constant \\
+$21$ & $392{,}370$   & $392{,}370$   & $392{,}370$   & all non-constant \\
 \hline
-total ($n \le 20$) & $142{,}812$ & $142{,}812$ & $142{,}812$ & \\
+total ($n \le 21$) & $535{,}182$ & $535{,}182$ & $535{,}182$ & \\
 \end{tabular}
 \end{center}
 \noindent In particular, $h_\varphi$ is non-constant on $V(K_b)$ alone
@@ -1499,12 +1499,24 @@ in every tested colouring (and likewise on $V(K_c)$); by
 Corollary~\ref{cor:single-cycle-non-constancy} each such colouring
 admits a Conjecture-\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}
 witness. This gives an empirical near-proof of the conjecture for
-$|V(G)| \le 20$ independent of (and consistent with) the direct
+$|V(G)| \le 21$ independent of (and consistent with) the direct
 witness-search check of Remark~\ref{rem:conj-3-6-empirical}. A
 structural proof of non-constancy on $V(K_b)$ (or on $V(K_c)$) would
 convert this into a proof of
 Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle}
 proper.
+
+\smallskip
+The $n = 21$ row was produced by
+\texttt{experiments/test\_n\_21\_to\_24.py}, which extends the
+empirical check to $|V(G)| \in \{21, 22, 23, 24\}$ and additionally
+verifies that the deciding-face conjecture
+(Conjecture~\ref{conj:deciding-face}) holds on every colouring; runs
+for $n \in \{22, 23, 24\}$ are still in flight at the time of writing.
+For $n = 21$: $192$ triangulations of minimum degree $5$ contribute
+$392{,}370$ chord-apex+Kempe colourings, all of which are non-constant
+on $V(K_b)$ alone and non-constant on $V(K_c)$ alone, and all of which
+admit a deciding face.
 \end{remark}
 
 \begin{remark}