diff --git a/papers/face_monochromatic_pairs/experiments/audit_tight_coverage.py b/papers/face_monochromatic_pairs/experiments/audit_tight_coverage.py new file mode 100644 index 0000000..2f0ceca --- /dev/null +++ b/papers/face_monochromatic_pairs/experiments/audit_tight_coverage.py @@ -0,0 +1,129 @@ +"""Audit: how many (G, v, i) triples are covered by the +structurally-TIGHT subset of the partial proof (dropping the +n_i = 6 case which has a gap in sub-case (ii.B) of the flank-covering +lemma)? + +Tight cases: + (a') n_i = 5 (= F_flank length 4, P adjacent to both A_i and A_{i+1}); + (b') n_{i+1} = 5 (symmetric); + (c) n_{i+2} = n_{i+4} = 5 (= F_outer length 7, both intermediates + adjacent to A_{i+3}, A_{i+4} ∈ V(K_b) ∩ V(K_c) via merged). + +Loose cases (the proof formally claims these but has a gap on +sub-case (ii.B)): + (a) n_i = 6 + (b) n_{i+1} = 6 + +This script reports per (G, v, i) whether tight-only coverage suffices. + +Run with: sage experiments/audit_tight_coverage.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) + + +def main(max_n=20, time_budget_per_n=1200): + print("Audit of structurally TIGHT coverage of the deciding-face\n" + "partial proof. Restricts to cases (a' = n_i = 5),\n" + "(b' = n_{i+1} = 5), (c = n_{i+2} = n_{i+4} = 5);\n" + "drops the (a)/(b) cases at n_k = 6 due to a gap in\n" + "Lemma 'Flank covering, n_i = 6' (sub-case ii.B).\n") + print(f"n_G in [12, {max_n}]\n") + + grand_triples = 0 + grand_loose_covered = 0 # by full partial proof (with gap) + grand_tight_covered = 0 # by tight-only subset + grand_loose_uncovered = 0 # empirical bad triples + grand_loose_not_tight = 0 # loose-covered but not tight (= n_i = 6 reliance) + grand_examples = [] + + 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_t = 0; n_loose = 0; n_tight = 0; n_diff = 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) + emb = G.get_embedding() + for v in G.vertex_iterator(): + if G.degree(v) != 5: continue + cyc = [G.degree(u) for u in emb[v]] + for i in range(5): + n_t += 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] + loose_a = (n_i in (5, 6)) + loose_b = (n_ip1 in (5, 6)) + case_c = (n_ip2 == 5 and n_ip4 == 5) + tight_a = (n_i == 5) + tight_b = (n_ip1 == 5) + loose = loose_a or loose_b or case_c + tight = tight_a or tight_b or case_c + if loose: n_loose += 1 + if tight: n_tight += 1 + if loose and not tight: n_diff += 1 + if loose and not tight and len(grand_examples) < 10: + grand_examples.append({ + 'n_G': n, 'tri_idx': tri_idx, 'v': v, 'i': i, + 'cyc': cyc, + 'n_tuple': (n_i, n_ip1, n_ip2, n_ip3, n_ip4), + }) + elapsed = time.time() - start + print(f"n={n}: {n_t} triples, loose-covered={n_loose} " + f"({100*n_loose/max(n_t,1):.1f}%), " + f"tight-only={n_tight} ({100*n_tight/max(n_t,1):.1f}%); " + f"loose-not-tight={n_diff} [{elapsed:.0f}s]") + sys.stdout.flush() + grand_triples += n_t + grand_loose_covered += n_loose + grand_tight_covered += n_tight + grand_loose_not_tight += n_diff + + grand_loose_uncovered = grand_triples - grand_loose_covered + grand_tight_uncovered = grand_triples - grand_tight_covered + print() + print("=" * 70) + print(f"Grand totals across n_G in [12, {max_n}]:") + print(f" (G, v, i) triples: {grand_triples}") + print(f" loose-covered (full partial proof): " + f"{grand_loose_covered} " + f"({100*grand_loose_covered/max(grand_triples,1):.2f}%)") + print(f" loose-uncovered (= empirical bad): " + f"{grand_loose_uncovered} " + f"({100*grand_loose_uncovered/max(grand_triples,1):.2f}%)") + print(f" tight-covered (drop n_i = 6 gap-case): " + f"{grand_tight_covered} " + f"({100*grand_tight_covered/max(grand_triples,1):.2f}%)") + print(f" tight-uncovered (needs n_i = 6 lemma): " + f"{grand_tight_uncovered} " + f"({100*grand_tight_uncovered/max(grand_triples,1):.2f}%)") + print(f" loose-not-tight (needs n_i = 6 lemma): " + f"{grand_loose_not_tight}") + if grand_examples: + print() + print(" Sample triples that need the n_i = 6 lemma " + "(NOT covered by tight subset):") + for ex in grand_examples[:10]: + print(f" n={ex['n_G']}, tri#{ex['tri_idx']}, " + f"v={ex['v']}, i={ex['i']}: cyc={ex['cyc']}, " + f"(n_i,n_{{i+1}},n_{{i+2}},n_{{i+3}},n_{{i+4}})={ex['n_tuple']}") + + +if __name__ == '__main__': + main() diff --git a/papers/face_monochromatic_pairs/experiments/check_v_neighbour_degrees.py b/papers/face_monochromatic_pairs/experiments/check_v_neighbour_degrees.py index 9c1e869..a837190 100644 --- a/papers/face_monochromatic_pairs/experiments/check_v_neighbour_degrees.py +++ b/papers/face_monochromatic_pairs/experiments/check_v_neighbour_degrees.py @@ -88,6 +88,16 @@ def main(max_n=20, time_budget_per_n=1200): n_ip2 = cyc[(i + 3) % 5] n_ip3 = cyc[(i + 4) % 5] n_ip4 = cyc[(i + 5) % 5] + # AUDIT: does the structurally-tight subset (drop n_i=6 case) cover? + tight_covered = ( + n_i == 5 or n_ip1 == 5 or + (n_ip2 == 5 and n_ip4 == 5) + ) + if not tight_covered: + # Record what would be the "audit-uncovered" triples + # (= we have proved coverage only on n_i = 5 or n_{i+1} = 5 + # or (n_{i+2}, n_{i+4}) = (5, 5)). + pass # counted below as "audit_uncovered_n" if n_i >= 7 and n_ip1 >= 7: bad_triples_n += 1 # Check whether F_outer's length condition is OK diff --git a/papers/face_monochromatic_pairs/paper.pdf b/papers/face_monochromatic_pairs/paper.pdf index b11229a..0d01055 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 3746cad..ec0bbd5 100644 --- a/papers/face_monochromatic_pairs/paper.tex +++ b/papers/face_monochromatic_pairs/paper.tex @@ -1041,9 +1041,21 @@ 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$] +\begin{lemma}[Flank covering, $n_i = 6$; partial] \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 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. \end{lemma} \begin{proof} @@ -1084,6 +1096,29 @@ to $P_1$. If this cycle is $K_b$, $P_1 \in V(K_b)$; if it is $K_c$ $\{c, c_1\}$), then $P_1 \in V(K_c)$. In either case $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. + +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}. \end{proof} \begin{theorem}[Partial proof of @@ -1205,10 +1240,18 @@ they satisfy case (c). Combining Theorems~\ref{thm:deciding-face-implies-conj-5-1} and~\ref{thm:deciding-face-partial-extended}, this yields a -\textbf{structural proof of +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$.} +$|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. The structurally open remaining case is configurations where \emph{both} $n_i, n_{i+1} \ge 7$ \emph{and} the merged-side