face_monochromatic_pairs: fix Conjecture 5.26 (strengthening) coverage claim

Previous commit (00229fa) incorrectly extended the empirical
verification of Conjecture 5.26 (strengthening, clauses 1-4) to n=21.

The running test (test_n_21_to_24.py) checks:
  - Non-constancy on V(K_b), V(K_c), V(K_b) ∪ V(K_c).
  - Deciding-face existence.

These verify Conjecture 5.1 (clauses 1-3) via Corollary 5.4 and via
the Heawood-face-sum route, respectively. They do NOT verify clause
(4) of the strengthening (Conjecture 5.26), which requires
constructing the subdivided graph and checking the new f_n's edge
colouring.

Conjecture 5.26 has been verified at n ≤ 20 (142,812 colourings) only,
via `check_conj_final_scaled.py` (which explicitly constructs the
clause-3 subdivision and checks clause-4). The n=21 results extend
the weaker checks but NOT the strengthening.

Paper fixes:
  - Abstract: clarified that strengthened conjecture is at n ≤ 20
    (142,812), unstrengthened (clauses 1-3) at n ≤ 21 (535,182).
  - Intro paragraph after "we propose": same clarification.

COMMENTARY.md fix:
  - Summary table: "Conjecture 5.26 (strengthening)" row reverted
    to "142,812 / 142,812 (n ≤ 20)". The other rows (about Heawood-
    based checks) remain at 535,182 / 535,182 (n ≤ 21).

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
This commit is contained in:
2026-05-25 08:40:01 -04:00
parent 00229fa460
commit d36c2513cc
3 changed files with 10 additions and 8 deletions
@@ -11,7 +11,7 @@ computationally vs what remains to be proven structurally.
| claim | status | empirical evidence | | claim | status | empirical evidence |
|---|---|---| |---|---|---|
| Conjecture 5.1 (clauses 13) | conjecture | ✓ 535,182 / 535,182 (n ≤ 21, direct witness search) | | Conjecture 5.1 (clauses 13) | conjecture | ✓ 535,182 / 535,182 (n ≤ 21, direct witness search) |
| Conjecture 5.3 (clauses 14, strengthening) | conjecture | ✓ 535,182 / 535,182 (n ≤ 21) | | Conjecture 5.26 (clauses 14, strengthening) | conjecture | ✓ 142,812 / 142,812 (n ≤ 20, via direct clause-4 check in `check_conj_final_scaled.py`) |
| 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) 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) | | **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) | | 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) |
Binary file not shown.
+9 -7
View File
@@ -60,10 +60,11 @@ same-coloured edges $e_1, e_2 \in \partial F$ whose subdivision-and-%
bridging produces a $4$-face $f_n$ whose boundary colouring places it 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 under the hypothesis of a $4$-face edge-suppression theorem; we use this
theorem to derive a proper $3$-edge-colouring of $G'$, contradicting theorem to derive a proper $3$-edge-colouring of $G'$, contradicting
minimality. We verify the conjecture computationally on all minimality. We verify the strengthened conjecture computationally on all
chord-apex+Kempe colourings of reduced duals with $|V(G)| \leq 21$ chord-apex+Kempe colourings of reduced duals with $|V(G)| \leq 20$
($535{,}182$ colourings, all pass: $142{,}812$ at $|V(G)| \leq 20$, ($142{,}812$ colourings, all pass); the unstrengthened form
plus $392{,}370$ new at $|V(G)| = 21$). (clauses 1--3) is verified up to $|V(G)| \leq 21$ ($535{,}182$
colourings, all pass).
\end{abstract} \end{abstract}
\maketitle \maketitle
@@ -115,9 +116,10 @@ $3$-edge-colouring of $G'$ can be recovered, contradicting the
non-$4$-colourability of $G$. The face-monochromatic-pair conjecture non-$4$-colourability of $G$. The face-monochromatic-pair conjecture
asserts the existence of the structural data ($F, e_1, e_2$) needed to 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 build $f_n$; the strengthening guarantees that $f_n$'s boundary colouring
falls under the suppression theorem's hypothesis. Both conjectures have falls under the suppression theorem's hypothesis. The strengthened conjecture has been verified computationally on all
been verified computationally on all chord-apex+Kempe colourings of chord-apex+Kempe colourings of reduced duals up to $|V(G)| \leq 20$
reduced duals up to $|V(G)| \leq 21$ ($535{,}182$ colourings). ($142{,}812$ colourings), and the unstrengthened (clauses 1--3) form
up to $|V(G)| \leq 21$ ($535{,}182$ colourings).
\paragraph{Organization.} Section~\ref{sec:minimal} fixes the \paragraph{Organization.} Section~\ref{sec:minimal} fixes the
minimal-counterexample framework: $G$ is a triangulation, minimal-counterexample framework: $G$ is a triangulation,