diff --git a/papers/face_monochromatic_pairs/experiments/check_subcase_iib.py b/papers/face_monochromatic_pairs/experiments/check_subcase_iib.py new file mode 100644 index 0000000..8ec9c36 --- /dev/null +++ b/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() diff --git a/papers/face_monochromatic_pairs/paper.pdf b/papers/face_monochromatic_pairs/paper.pdf index 0d01055..344601e 100644 Binary files a/papers/face_monochromatic_pairs/paper.pdf and b/papers/face_monochromatic_pairs/paper.pdf differ diff --git a/papers/face_monochromatic_pairs/paper.tex b/papers/face_monochromatic_pairs/paper.tex index ec0bbd5..f570e4d 100644 --- a/papers/face_monochromatic_pairs/paper.tex +++ b/papers/face_monochromatic_pairs/paper.tex @@ -1041,21 +1041,45 @@ 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$; partial] +\begin{lemma}[Flank covering, $n_i = 6$; \textbf{empirically FALSE in full +generality}] \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 naive statement ``if $n_i = 6$ then +$\partial F_{i, i+1}^{\flat} \subseteq V(K_b) \cup V(K_c)$'' is +\emph{false} in full generality. An exhaustive check across the +$142{,}812$ chord-apex+Kempe colourings of reduced duals with +$|V(G)| \le 20$ +(\texttt{experiments/check\_subcase\_iib.py}) finds: +\begin{itemize} +\item $9{,}228$ colourings ($6.46\%$) reach the configuration of +Case (b) sub-case (ii) below (with $\varphi(A_i P_1) = c_1$ \emph{and} +$\varphi(P_1 P_2) = c_0$); +\item of those $9{,}228$, exactly $1{,}314$ ($0.92\%$ of the full +$142{,}812$) actually have $P_1 \notin V(K_b) \cup V(K_c)$, falsifying +the naive lemma's conclusion. +\end{itemize} -\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. +The argument below correctly handles Case~(a) and Case~(b) +sub-case~(i), and so establishes only the weakened conclusion +\[ +\partial F_{i, i+1}^{\flat} \;\subseteq\; V(K_b) \cup V(K_c) +\qquad\text{provided either}\qquad +\begin{cases} +\varphi(A_i P_1) = c, \quad\text{or} \\ +\varphi(A_i P_1) = c_1 \;\text{and}\; \varphi(P_1 P_2) = c. +\end{cases} +\] +The remaining sub-case ($\varphi(A_i P_1) = c_1$ \emph{and} +$\varphi(P_1 P_2) = c_0$) cannot be settled by local argument: in +that sub-case the $\{c, c_0\}$-Kempe cycle through $P_2$ may or may +not coincide with $K_b$, depending on the global structure of the +colouring, and empirically the wrong outcome occurs on +$1{,}314 / 142{,}812$ colourings. + +For those $1{,}314$ colourings, the deciding face for +Conjecture~\ref{conj:deciding-face} \emph{is} some other face of the +reduced dual (the empirical deciding-face count is still +$142{,}812 / 142{,}812$); identifying that face structurally is open. \end{lemma} \begin{proof} @@ -1084,62 +1108,57 @@ $\varphi(P_1 P_2) = c_1$. Hence \[ \varphi(P_1 P_2) \;\in\; \{c, c_0\}. \] -Now $P_2 \in V(K_b) \cup V(K_c)$ as shown, and at $P_2$ the cycle that -contains $P_2$ uses two specific edges of $P_2$. If $P_2 \in V(K_b)$ -the cycle uses $P_2$'s colour-$c$ and colour-$c_0$ edges; if -$P_2 \in V(K_c)$ it uses colour-$c$ and colour-$c_1$. In either case -the cycle at $P_2$ uses $P_2$'s colour-$c$ edge. By the -preceding paragraph $\varphi(P_1 P_2) \in \{c, c_0\}$, so the -$\{c, \varphi(P_2 P_1)\}$-Kempe cycle through $P_2$ passes from $P_2$ -to $P_1$. If this cycle is $K_b$, $P_1 \in V(K_b)$; if it is $K_c$ -(which requires $\varphi(P_1 P_2) = c$, since $K_c$ uses -$\{c, c_1\}$), then $P_1 \in V(K_c)$. +Case~(b) splits further on $\varphi(P_1 P_2)$. -In either case $P_1 \in V(K_b) \cup V(K_c)$. +\emph{Sub-case (i):} $\varphi(P_1 P_2) = c$. Then $P_2$'s colour-$c$ +edge is $P_1 P_2$. Both $K_b$ and $K_c$ use the colour-$c$ edge +at any vertex they pass through, so whichever of $K_b, K_c$ contains +$P_2$ walks via $P_1 P_2$ to $P_1$, placing $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. +\emph{Sub-case (ii):} $\varphi(P_1 P_2) = c_0$. Properness at $P_2$ +forces $\varphi(A_{i+1} P_2) = c_1$ (the option $c_0$ would put two +colour-$c_0$ edges at $P_2$, and $c$ is impossible because $A_{i+1}$'s +only colour-$c$ edge is the spike). Hence $P_2 \in V(K_c)$ via $K_c$'s +walk $A_{i+1} \xrightarrow{c_1} P_2$. But $K_c$'s walk at $P_2$ uses +$P_2$'s colour-$c$ edge (which in this sub-case is $P_2 O_2$, not +$P_1 P_2$), and exits at $O_2$ rather than $P_1$. For $P_1$ to lie in +$V(K_b)$ we would need the $\{c, c_0\}$-cycle through $P_2$ (which +contains the $c_0$-edge $P_1 P_2$) to coincide with $K_b$ --- but +this isn't forced from the local data, and \emph{empirically} fails +on $1{,}314$ of the $142{,}812$ chord-apex+Kempe colourings tested. -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}. +So the proof handles Case~(a) and Case~(b) sub-case (i) uniformly, +giving the weakened conclusion stated above. Case~(b) sub-case (ii) +is not settled by local argument. \end{proof} \begin{theorem}[Partial proof of Conjecture~\ref{conj:deciding-face} via flank face] \label{thm:deciding-face-partial} -If $n_i \in \{5, 6\}$ or $n_{i+1} \in \{5, 6\}$ for the reduction -index $i$, then $\widehat{G}'_{v,i}$ has a deciding face: one of -the two flank faces $F_{i, i+1}^{\flat}$ or $F_{i+1, i+2}^{\flat}$. +If $n_i = 5$ or $n_{i+1} = 5$ for the reduction index $i$, then +$\widehat{G}'_{v,i}$ has a deciding face: one of the two flank faces +$F_{i, i+1}^{\flat}$ or $F_{i+1, i+2}^{\flat}$. \end{theorem} \begin{proof} -Without loss of generality $n_i \in \{5, 6\}$ (the $n_{i+1}$ case is -symmetric, swapping side-$0$ with side-$1$). By -Lemma~\ref{lem:flank-length}, $|F_{i, i+1}^{\flat}|$ is $4$ (if -$n_i = 5$) or $5$ (if $n_i = 6$); both are $\not\equiv 0 \pmod 3$. -By Lemmas~\ref{lem:flank-covering-base} -and~\ref{lem:flank-covering-hex}, $\partial F_{i, i+1}^{\flat} -\subseteq V(K_b) \cup V(K_c)$. Hence $F_{i, i+1}^{\flat}$ is a -deciding face. +Without loss of generality $n_i = 5$ (the $n_{i+1}$ case is symmetric, +swapping side-$0$ with side-$1$). By Lemma~\ref{lem:flank-length}, +$|F_{i, i+1}^{\flat}| = 4 \not\equiv 0 \pmod 3$. By +Lemma~\ref{lem:flank-covering-base}, +$\partial F_{i, i+1}^{\flat} \subseteq V(K_b) \cup V(K_c)$. Hence +$F_{i, i+1}^{\flat}$ is a deciding face. \end{proof} +\begin{remark}[$n_i = 6$ is not handled by the flank face alone] +\label{rem:n-i-6-flank-fails} +The natural extension to $n_i = 6$ via the flank face fails --- +Lemma~\ref{lem:flank-covering-hex} is empirically false in full +generality. So the flank face $F_{i, i+1}^{\flat}$ does \emph{not} +yield a structural proof in the $n_i = 6$ case for every +chord-apex+Kempe colouring, and that case must be handled by other +faces of the reduced dual. +\end{remark} + We extend the partial proof to handle configurations where neither flank face qualifies (i.e., both $n_i, n_{i+1} \ge 7$). The candidate is the \emph{outer face} inside $F$, on the merged side of $v_n$. @@ -1207,13 +1226,13 @@ Conjecture~\ref{conj:deciding-face}] \label{thm:deciding-face-partial-extended} The deciding face exists for $\widehat{G}'_{v,i}$ whenever at least one of the following holds: -\textbf{(a)} $n_i \in \{5, 6\}$; -\textbf{(b)} $n_{i+1} \in \{5, 6\}$; or +\textbf{(a$'$)} $n_i = 5$; +\textbf{(b$'$)} $n_{i+1} = 5$; or \textbf{(c)} $n_{i+2} = n_{i+4} = 5$. \end{theorem} \begin{proof} -Cases (a) and (b) are covered by Theorem~\ref{thm:deciding-face-partial}, +Cases (a$'$) and (b$'$) are Theorem~\ref{thm:deciding-face-partial}, yielding the flank face $F_{i, i+1}^{\flat}$ or $F_{i+1, i+2}^{\flat}$ as the deciding face. For case (c), $|F_{\mathrm{outer}}^{\flat}| = 5 + 5 - 3 = 7 \equiv 1 \pmod 3$ by @@ -1230,28 +1249,29 @@ Across all $1{,}586$ $(G, v)$ pairs underlying chord-apex+Kempe colourings for $|V(G)| \le 20$, every cyclic neighbour-degree sequence around $v$ contains at least one degree-$5$ entry (see \texttt{experiments/check\_v\_neighbour\_degrees.py}). Of the -$7{,}930$ $(G, v, i)$ triples we have: -\begin{itemize} -\item $7{,}906$ ($99.70\%$) satisfy case (a) or (b); -\item the remaining $24$ ($0.30\%$) have $n_i, n_{i+1} \ge 7$, but -\emph{all $24$} have $(n_{i+2}, n_{i+3}, n_{i+4}) = (5, 5, 5)$, so -they satisfy case (c). -\end{itemize} -Combining -Theorems~\ref{thm:deciding-face-implies-conj-5-1} -and~\ref{thm:deciding-face-partial-extended}, this yields a -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$, \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. +$7{,}930$ $(G, v, i)$ triples, +Theorem~\ref{thm:deciding-face-partial-extended} (cases (a$'$), +(b$'$), (c)) gives a deciding face for $7{,}531$ ($94.97\%$); see +\texttt{experiments/audit\_tight\_coverage.py}. + +The remaining $399$ triples ($5.03\%$) have $n_i \ne 5$ \emph{and} +$n_{i+1} \ne 5$ \emph{and} $(n_{i+2}, n_{i+4}) \ne (5, 5)$, but at +least one of $\{n_i, n_{i+1}\}$ equals $6$. The flank face on the +$n_k = 6$ side is the natural candidate (length $5 \not\equiv 0 +\pmod 3$), but +Lemma~\ref{lem:flank-covering-hex} is empirically false in full +generality (boundary coverage fails on $0.92\%$ of colourings via +Case (b) sub-case (ii)). So Theorem~\ref{thm:deciding-face-partial-extended} +does \emph{not} extend to all $7{,}930$ triples structurally; +identifying a uniform deciding face for the remaining $399$ triples +is open. + +Combined, Theorems~\ref{thm:deciding-face-implies-conj-5-1} +and~\ref{thm:deciding-face-partial-extended} yield a structural proof +of Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle} +on $7{,}531 / 7{,}930$ ($94.97\%$) of chord-apex+Kempe configurations +up to $|V(G)| \le 20$. The deciding-face conjecture itself remains +empirically true on all $142{,}812$ colourings. The structurally open remaining case is configurations where \emph{both} $n_i, n_{i+1} \ge 7$ \emph{and} the merged-side