diff --git a/papers/face_monochromatic_pairs/experiments/check_bad_subcase_deciding_face.py b/papers/face_monochromatic_pairs/experiments/check_bad_subcase_deciding_face.py new file mode 100644 index 0000000..184fe64 --- /dev/null +++ b/papers/face_monochromatic_pairs/experiments/check_bad_subcase_deciding_face.py @@ -0,0 +1,302 @@ +"""For the 1,314 colourings on which Lemma (Flank covering, n_i = 6) +empirically fails (sub-case (ii.B) + P_1 ∉ V(K_b) ∪ V(K_c)), identify +which face actually IS the deciding face. If there's a consistent +type (e.g., always F_outer^♭ or F_merged^♭), we can add a new lemma. + +For each "bad" colouring, classify all faces of the reduced dual into +types: + - flank-lower (= F_flank_{i, i+1}^♭, length n_i - 1) + - flank-upper (= F_flank_{i+1, i+2}^♭, length n_{i+1} - 1) + - outer (= F_outer^♭, length n_{i+2} + n_{i+4} - 3) + - merged (= F_merged^♭, length n_{i+3} - 2) + - other (= original G' face not adjacent to F_v, or some + other face from the reduction process) + +Then for each face, check whether it is "deciding" (∂f ⊆ V(K_b) ∪ V(K_c) +AND |f| ≢ 0 mod 3) and report the distribution of deciding face types +across the 1,314 bad colourings. + +Run with: sage experiments/check_bad_subcase_deciding_face.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 classify_face(H, face, named, P_arc_lower, P_arc_upper, + arc_outer_a, arc_outer_b, arc_merged): + """Classify a face by which "type" it is. + P_arc_*: arc vertices for the various near-spike faces. + """ + fv = {v for e in face for v in e} + # Check if the face contains the spike edge AND side_0 (= flank lower) + face_edges = {frozenset(e) for e in face} + if {named['side_0'], named['spike']}.issubset(face_edges): + return 'flank-lower' + if {named['spike'], named['side_1']}.issubset(face_edges): + return 'flank-upper' + if {named['side_0'], named['side_1'], named['merged']}.issubset(face_edges): + return 'outer' + if named['merged'] in face_edges and len(face) <= 6: + # Could be merged face -- check more carefully + # The merged face contains only the merged edge from named, and + # the rest is an arc + if {named['side_0']}.issubset(face_edges): + return 'outer' + if {named['side_1']}.issubset(face_edges): + return 'outer' + return 'merged' + return 'other' + + +def find_deciding_faces(H, V_union): + """Return list of (face, length, type-info) for all deciding faces.""" + H.is_planar(set_embedding=True) + out = [] + for face in H.faces(): + verts = {u for (u, v) in face} | {v for (u, v) in face} + if not verts.issubset(V_union): + continue + L = len(face) + if L % 3 == 0: + continue + out.append((face, L)) + return out + + +def named_v_set(named, v_n=9999): + 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']) + return {'v_n': v_n, 'A_i': A_i, 'A_ip1': A_ip1, 'A_ip2': A_ip2, + 'A_ip3': A_ip3, 'A_ip4': A_ip4} + + +def classify_deciding_face(face, named_verts, named_edges): + """Best-effort classification of which "type" the face is.""" + face_edges_set = {frozenset(e) for e in face} + has_side_0 = named_edges['side_0'] in face_edges_set + has_side_1 = named_edges['side_1'] in face_edges_set + has_spike = named_edges['spike'] in face_edges_set + has_merged = named_edges['merged'] in face_edges_set + if has_side_0 and has_spike and not has_side_1 and not has_merged: + return 'flank-lower' + if has_spike and has_side_1 and not has_side_0 and not has_merged: + return 'flank-upper' + if has_side_0 and has_side_1 and has_merged and not has_spike: + return 'outer' + if has_merged and not has_side_0 and not has_side_1 and not has_spike: + return 'merged' + # Anything else -- a face of the reduced dual using zero or partial + # near-spike edges + if not (has_side_0 or has_side_1 or has_spike or has_merged): + return 'G-prime-face' + return f'mixed({"+".join(sorted([n for n, x in [("s0", has_side_0), ("s1", has_side_1), ("sp", has_spike), ("m", has_merged)] if x]))})' + + +def test_one(D): + D.is_planar(set_embedding=True) + bad_colourings = 0 + deciding_face_dist = {} # type -> count + deciding_length_dist = {} # (type, length) -> count + no_deciding = 0 + per_colouring_dist = {} # frozenset of types -> count + full_coverage_count = {} # bool -> count + 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: + v_n = 9999 + nv = named_v_set(named, v_n) + A_i, A_ip1 = nv['A_i'], nv['A_ip1'] + merged_idx = edge_idx(edges, named['merged']) + c_color = col[merged_idx] + c_0_color = col[edge_idx(edges, named['side_0'])] + c_1_color = col[edge_idx(edges, named['side_1'])] + a = c_color + other = [x for x in range(3) if x != a] + # K_b, K_c + 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) + V_union = V_b | V_c + + # Check for sub-case (ii.B) on the lower flank + # Find the lower flank face + target = {named['side_0'], named['spike']} + lower_flank = None + for f in H.faces(): + f_edges = {frozenset(e) for e in f} + if target.issubset(f_edges): + lower_flank = f + break + if lower_flank is None or len(lower_flank) != 5: + continue + # Identify P_1, P_2 + arc_verts = [e[0] for e in lower_flank] + if v_n not in arc_verts: + continue + k = arc_verts.index(v_n) + cyc = arc_verts[k:] + arc_verts[:k] + if cyc[1] == A_i and cyc[4] == A_ip1: + P_1, P_2 = cyc[2], cyc[3] + elif cyc[1] == A_ip1 and cyc[4] == A_i: + P_2, P_1 = cyc[2], cyc[3] + else: + continue + # Check sub-case (ii.B): φ(A_i P_1) = c_1 AND φ(P_1 P_2) = c_0 + 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_color or col[e_P1P2] != c_0_color: + continue + # Is P_1 ∉ V(K_b) ∪ V(K_c)? + if P_1 in V_union: + continue + # This is a "bad" colouring (= 1314 total) + bad_colourings += 1 + # Find all deciding faces + deciding = find_deciding_faces(H, V_union) + if not deciding: + no_deciding += 1 + continue + # Classify each deciding face + types_present = set() + for f, L in deciding: + t = classify_deciding_face(f, nv, named) + deciding_face_dist[t] = deciding_face_dist.get(t, 0) + 1 + key = (t, L) + deciding_length_dist[key] = deciding_length_dist.get(key, 0) + 1 + types_present.add(t) + # Track per-colouring which types are available + key = frozenset(types_present) + per_colouring_dist[key] = per_colouring_dist.get(key, 0) + 1 + full_coverage = (len(V_union) == H.order()) + full_coverage_count[full_coverage] = ( + full_coverage_count.get(full_coverage, 0) + 1) + return (bad_colourings, deciding_face_dist, deciding_length_dist, + no_deciding, per_colouring_dist, full_coverage_count) + + +def main(max_n=20, time_budget_per_n=1800): + print("For chord-apex+Kempe colourings with sub-case (ii.B) AND " + "P_1 ∉ V(K_b) ∪ V(K_c)\n" + "(= the 1,314 colourings on which Lemma flank-covering-hex " + "is empirically FALSE),\n" + "classify the deciding faces.\n") + grand_bad = 0 + grand_face_dist = {} + grand_length_dist = {} + grand_no_deciding = 0 + grand_per_col = {} + grand_full_cov = {} + 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_bad = 0 + n_no_d = 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) + nb, fd, ld, nd, pc, fc = test_one(D) + n_bad += nb + n_no_d += nd + for k, v in fd.items(): + grand_face_dist[k] = grand_face_dist.get(k, 0) + v + for k, v in ld.items(): + grand_length_dist[k] = grand_length_dist.get(k, 0) + v + for k, v in pc.items(): + grand_per_col[k] = grand_per_col.get(k, 0) + v + for k, v in fc.items(): + grand_full_cov[k] = grand_full_cov.get(k, 0) + v + elapsed = time.time() - start + print(f"n={n}: {n_bad} bad colourings [{elapsed:.0f}s]") + sys.stdout.flush() + grand_bad += n_bad + grand_no_deciding += n_no_d + print() + print("=" * 70) + print(f"Total bad colourings: {grand_bad}") + print(f"Of those, NO deciding face found: {grand_no_deciding}") + if grand_face_dist: + print() + print("Deciding-face TYPE distribution (counts can exceed bad_count " + "since each colouring can have multiple deciding faces):") + for t in sorted(grand_face_dist, key=lambda x: -grand_face_dist[x]): + c = grand_face_dist[t] + print(f" {t}: {c}") + print() + print("Deciding-face (TYPE, LENGTH) distribution:") + for k in sorted(grand_length_dist, key=lambda x: -grand_length_dist[x]): + t, L = k + c = grand_length_dist[k] + print(f" {t}, |f|={L}: {c}") + print() + print(f"Full coverage V(K_b) ∪ V(K_c) = V on bad colourings:") + for k, v in sorted(grand_full_cov.items()): + print(f" {k}: {v}") + print() + print("Per-colouring deciding-face TYPES (count of colourings with " + "exactly this set of types available):") + for k in sorted(grand_per_col, key=lambda x: -grand_per_col[x]): + c = grand_per_col[k] + types_str = ', '.join(sorted(k)) + print(f" {{{types_str}}}: {c}") + # How many colourings have G-prime-face as a deciding face? + n_with_gprime = sum(v for k, v in grand_per_col.items() + if 'G-prime-face' in k) + print() + print(f"Colourings with at least one G-prime-face deciding: " + f"{n_with_gprime} / {grand_bad} " + f"({100*n_with_gprime/max(grand_bad, 1):.2f}%)") + n_with_outer = sum(v for k, v in grand_per_col.items() + if 'outer' in k) + print(f"Colourings with at least one outer-face deciding: " + f"{n_with_outer} / {grand_bad} " + f"({100*n_with_outer/max(grand_bad, 1):.2f}%)") + n_with_merged = sum(v for k, v in grand_per_col.items() + if 'merged' in k) + print(f"Colourings with at least one merged-face deciding: " + f"{n_with_merged} / {grand_bad} " + f"({100*n_with_merged/max(grand_bad, 1):.2f}%)") + n_with_upper = sum(v for k, v in grand_per_col.items() + if 'flank-upper' in k) + print(f"Colourings with at least one flank-upper deciding: " + f"{n_with_upper} / {grand_bad} " + f"({100*n_with_upper/max(grand_bad, 1):.2f}%)") + + +if __name__ == '__main__': + main() diff --git a/papers/face_monochromatic_pairs/paper.pdf b/papers/face_monochromatic_pairs/paper.pdf index 344601e..59cb763 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 f570e4d..d0c52b0 100644 --- a/papers/face_monochromatic_pairs/paper.tex +++ b/papers/face_monochromatic_pairs/paper.tex @@ -1258,20 +1258,53 @@ 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. +\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)). + +\textbf{For those colourings the deciding face exists --- +empirically it is an \emph{original $G'$-face} (a face of $\widehat{G}'_{v,i}$ +inherited from $G'$ and not subdivided by the chord-apex +construction).} Concretely +(\texttt{experiments/check\_bad\_subcase\_deciding\_face.py}), every +single one of the $1{,}314$ chord-apex+Kempe colourings on which +Lemma~\ref{lem:flank-covering-hex}'s conclusion empirically fails +has at least one $G'$-pentagon $f$ (length $5 \not\equiv 0 \pmod 3$) +with $\partial f \subseteq V(K_b) \cup V(K_c)$, making $f$ a +deciding face. (Independently, $94.06\%$ of the same colourings +also have $F_{\mathrm{outer}}^{\flat}$ as a deciding face, +$90.41\%$ have $F_{i+1, i+2}^{\flat}$ as one, and $39.27\%$ have +$F_{\mathrm{merged}}^{\flat}$ as one --- redundancy is the norm.) + +This suggests the following structural claim, currently open: + +\begin{conjecture}[$G'$-pentagon fallback] +\label{conj:gprime-pentagon-fallback} +For every chord-apex+Kempe colouring of every reduced dual +$\widehat{G}'_{v,i}$, at least one $G'$-pentagon $f$ (= pentagonal +face of $G'$ not equal to $F_v$ or to any of $F_i, \ldots, F_{i+4}$) +satisfies $\partial f \subseteq V(K_b) \cup V(K_c)$. +\end{conjecture} + +If Conjecture~\ref{conj:gprime-pentagon-fallback} is true, then together +with Theorem~\ref{thm:deciding-face-partial-extended} it gives a +structural proof of the deciding-face conjecture for every +chord-apex+Kempe configuration, hence (via +Theorem~\ref{thm:deciding-face-implies-conj-5-1}) a structural proof +of Conjecture~\ref{conj:face-monochromatic-pair-on-merged-kempe-cycle} +in full generality. Empirically this fallback closes the residual +$0.92\%$ ($1{,}314$ of $142{,}812$) of chord-apex+Kempe colourings +that the near-spike argument leaves 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. +up to $|V(G)| \le 20$; the remaining $5.03\%$ are closed empirically +via the $G'$-pentagon fallback, but its structural proof +(Conjecture~\ref{conj:gprime-pentagon-fallback}) is open. 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