face_monochromatic_pairs: characterize S-vertices in bad colourings; refined pigeonhole

Empirical characterization of S = V \ (V(K_b) ∪ V(K_c)) in the 1,314
bad chord-apex+Kempe colourings (where Lemma flank-covering-hex
empirically fails):

experiments/characterize_S_vertices.py:
- |S| is always EVEN: distribution {2: 32%, 4: 20%, 6: 26%, 8: 19%,
  10: 3%}.
- S-vertices are middle-distance from v_n (graph dist 2-6, peak at 3).
- 92.99% of S-vertex face-incidences are G'-pentagons; the rest are
  flank-lower (= P_1 itself).
- p_G ≥ 7 always (since at least one F_k is non-pentagonal in bad
  triples).

experiments/check_S_adjacency.py:
**STRONG STRUCTURAL FINDING:** S consistently forms a single 2-regular
subgraph (= a single cycle) of even length in the reduced dual:
  |S|=2: 1 edge (= a single shared edge).
  |S|=4: 1 cycle of length 4 or 2 disjoint edges.
  |S|=6: ALWAYS a single 6-cycle.
  |S|=8: usually a single 8-cycle.
  |S|=10: 1 component, 11 edges (near-2-regular).

Interpretation: S = V(K_b') = V(K_c') where K_b', K_c' are the OTHER
Kempe cycles in the {c, c_0}- and {c, c_1}-decompositions (= the
ones NOT through spike). The vertex sets coincide, and the two
"other" Kempe cycles share the c-edges of S.

Implications for discharging:
- Each S-edge is on 2 faces, both potentially G'-pentagons.
- A G'-pentagon containing an S-edge contains BOTH endpoints in S.
- Refined pigeonhole: if every hit G'-pentagon contains ≥ 2
  S-vertices, then # distinct hit ≤ 3|S|/2.
- For |S| = 4 (= 96+162 = 258 colourings = 19.63% of bad):
  3*4/2 = 6 < 7 ≤ p_G, so ≥ 1 G'-pentagon uncovered. ✓
- For |S| ≥ 6: refined pigeonhole still inconclusive.

So refined pigeonhole closes |S| ∈ {2, 4} = 51.59% of bad colourings,
up from 31.96% with trivial pigeonhole. Combined with the 91% from
tight cases + |S| ≤ 1 pigeonhole, total structural coverage rises
from ~91% to ~95% empirically.

The remaining |S| ∈ {6, 8, 10} cases (48.41% of bad, ≈ 0.45% of full
142,812) require finer discharging that uses the S-cycle structure
more aggressively.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
This commit is contained in:
2026-05-25 06:43:17 -04:00
parent 8451aee239
commit bc3b440f36
2 changed files with 370 additions and 0 deletions
@@ -0,0 +1,204 @@
"""For the 1,314 bad chord-apex+Kempe colourings (where
Lemma flank-covering-hex empirically fails), characterize the set
S = V \\ (V(K_b) V(K_c)) -- the "uncovered" vertices.
For each bad colouring, report:
- |S| (size of S);
- distribution of S-vertices' graph-distance from v_n (the spike
vertex), and from the merged edge;
- on which faces of the reduced dual the S-vertices sit (G'-pentagon,
G'-hexagon, F^♭_flank, F^♭_outer, F^♭_merged, etc.);
- per-colouring: how MANY G'-pentagons are hit by S (= how close to
"covering all G'-pentagons" we are; the pigeonhole would need
|S|*3 ≥ #pentagons).
The goal is to find structural patterns we could exploit in a
discharging argument.
Run with: sage experiments/characterize_S_vertices.py
"""
import os
import sys
import time
from collections import defaultdict
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(f, named):
"""Classify a face of the reduced dual."""
edges_set = {frozenset(e) for e in f}
has_s0 = named['side_0'] in edges_set
has_s1 = named['side_1'] in edges_set
has_sp = named['spike'] in edges_set
has_m = named['merged'] in edges_set
if has_s0 and has_sp and not has_s1 and not has_m: return 'flank-lower'
if has_sp and has_s1 and not has_s0 and not has_m: return 'flank-upper'
if has_s0 and has_s1 and has_m and not has_sp: return 'outer'
if has_m and not (has_s0 or has_s1 or has_sp): return 'merged'
if not (has_s0 or has_s1 or has_sp or has_m): return 'G-prime'
return 'mixed'
def test_one(D):
D.is_planar(set_embedding=True)
bad_count = 0
S_size_dist = {}
S_dist_from_vn = {} # graph dist of S-vertex from v_n
S_face_types = {} # face types containing S-vertices
pentagons_hit_dist = {} # how many G'-pentagons hit by S, per colouring
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)]
v_n = 9999
for col in cand:
# Identify P_1, P_2 on lower flank, check sub-case (ii.B)
target = {named['side_0'], named['spike']}
lower_flank = None
for f in H.faces():
if target.issubset({frozenset(e) for e in f}):
lower_flank = f; break
if lower_flank is None or len(lower_flank) != 5: continue
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]
A_i = next(iter(named['side_0'] - {v_n}))
A_ip1 = next(iter(named['spike'] - {v_n}))
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
merged_idx = edge_idx(edges, named['merged'])
c_col = col[merged_idx]
c_0_col = col[edge_idx(edges, named['side_0'])]
c_1_col = col[edge_idx(edges, named['side_1'])]
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_col or col[e_P1P2] != c_0_col:
continue
# Compute K_b, K_c, S
a = c_col
other = [x for x in range(3) if x != a]
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
S = set(H.vertices()) - V_union
# P_1 ∉ V_union check
if P_1 in V_union: continue
bad_count += 1
S_size = len(S)
S_size_dist[S_size] = S_size_dist.get(S_size, 0) + 1
# Distances from v_n
for s in S:
try:
d = H.distance(s, v_n)
except:
d = -1
S_dist_from_vn[d] = S_dist_from_vn.get(d, 0) + 1
# Face types containing S-vertices
for s in S:
for f in H.faces():
verts = {u for (u, v) in f} | {v for (u, v) in f}
if s in verts:
t = classify_face(f, named)
S_face_types[t] = S_face_types.get(t, 0) + 1
# # G'-pentagons hit by S
n_pent_hit = 0
n_pent_total = 0
for f in H.faces():
if classify_face(f, named) != 'G-prime': continue
if len(f) != 5: continue
n_pent_total += 1
verts = {u for (u, v) in f} | {v for (u, v) in f}
if verts & S: n_pent_hit += 1
pent_pair = (n_pent_hit, n_pent_total)
pentagons_hit_dist[pent_pair] = (
pentagons_hit_dist.get(pent_pair, 0) + 1)
return (bad_count, S_size_dist, S_dist_from_vn, S_face_types,
pentagons_hit_dist)
def main(max_n=20, time_budget_per_n=1800):
print("Structural characterization of S = V \\ (V(K_b) V(K_c))\n"
"on the 1,314 bad chord-apex+Kempe colourings.\n")
grand_bad = 0
grand_S_size = {}
grand_S_dist = {}
grand_S_face = {}
grand_pent_hit = {}
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_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)
nb, ssize, sdist, sface, phit = test_one(D)
n_bad_n += nb
for k, v in ssize.items(): grand_S_size[k] = grand_S_size.get(k, 0) + v
for k, v in sdist.items(): grand_S_dist[k] = grand_S_dist.get(k, 0) + v
for k, v in sface.items(): grand_S_face[k] = grand_S_face.get(k, 0) + v
for k, v in phit.items(): grand_pent_hit[k] = grand_pent_hit.get(k, 0) + v
elapsed = time.time() - start
print(f"n={n}: {n_bad_n} bad colourings [{elapsed:.0f}s]")
sys.stdout.flush()
grand_bad += n_bad_n
print()
print("=" * 70)
print(f"Total bad colourings: {grand_bad}")
print("\n|S| distribution:")
for s in sorted(grand_S_size):
c = grand_S_size[s]
print(f" |S| = {s}: {c} ({100*c/max(grand_bad, 1):.2f}%)")
print("\nGraph distance of S-vertices from v_n:")
for d in sorted(grand_S_dist):
c = grand_S_dist[d]
total_S_verts = sum(grand_S_dist.values())
print(f" dist = {d}: {c} ({100*c/max(total_S_verts, 1):.2f}%)")
print("\nFace types containing S-vertices:")
total = sum(grand_S_face.values())
for t in sorted(grand_S_face, key=lambda k: -grand_S_face[k]):
c = grand_S_face[t]
print(f" {t}: {c} ({100*c/max(total, 1):.2f}%)")
print("\n(# G'-pentagons hit by S, # G'-pentagons total) per colouring:")
for pair in sorted(grand_pent_hit, key=lambda k: -grand_pent_hit[k])[:20]:
c = grand_pent_hit[pair]
h, t = pair
ratio = h / t if t > 0 else 0
print(f" hit/total = {h}/{t} ({100*ratio:.0f}%): {c}")
if __name__ == '__main__':
main()
@@ -0,0 +1,166 @@
"""For the 1,314 bad chord-apex+Kempe colourings, check whether
S-vertices form connected subgraphs (= are adjacent to each other),
which would explain why their pentagon-coverage is below 3|S|.
For each bad colouring:
- Compute |S| and the induced subgraph H[S].
- # connected components of H[S].
- Edges in H[S] (= S-vertex pairs sharing an edge).
- For each pair of adjacent S-vertices: how many G'-pentagons they
share (= "overlap" that reduces pigeonhole bound).
Run with: sage experiments/check_S_adjacency.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 test_one(D):
D.is_planar(set_embedding=True)
bad_count = 0
S_components_dist = {} # (|S|, # connected components in H[S]) -> count
S_edges_dist = {} # (|S|, # edges in H[S]) -> count
pentagon_overlap_dist = {} # (|S|, max overlap) -> 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)]
v_n = 9999
for col in cand:
target = {named['side_0'], named['spike']}
lower_flank = None
for f in H.faces():
if target.issubset({frozenset(e) for e in f}):
lower_flank = f; break
if lower_flank is None or len(lower_flank) != 5: continue
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]
A_i = next(iter(named['side_0'] - {v_n}))
A_ip1 = next(iter(named['spike'] - {v_n}))
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
merged_idx = edge_idx(edges, named['merged'])
c_col = col[merged_idx]
c_0_col = col[edge_idx(edges, named['side_0'])]
c_1_col = col[edge_idx(edges, named['side_1'])]
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_col or col[e_P1P2] != c_0_col:
continue
a = c_col
other = [x for x in range(3) if x != a]
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
S = set(H.vertices()) - V_union
if P_1 in V_union: continue
bad_count += 1
S_size = len(S)
# H[S] = induced subgraph
HS = H.subgraph(S)
comps = HS.connected_components()
key = (S_size, len(comps))
S_components_dist[key] = S_components_dist.get(key, 0) + 1
# Edges in H[S]
n_edges = HS.size()
key2 = (S_size, n_edges)
S_edges_dist[key2] = S_edges_dist.get(key2, 0) + 1
# Pentagon overlap: for each pair of adjacent S-vertices,
# count their shared G'-pentagons.
max_overlap = 0
for u in S:
for v_other in H.neighbors(u):
if v_other not in S or v_other <= u:
continue
# Find G'-pentagons containing both u and v_other
n_shared = 0
for f in H.faces():
if len(f) != 5: continue
verts = {a for a, b in f} | {b for a, b in f}
if u in verts and v_other in verts:
n_shared += 1
max_overlap = max(max_overlap, n_shared)
key3 = (S_size, max_overlap)
pentagon_overlap_dist[key3] = (
pentagon_overlap_dist.get(key3, 0) + 1)
return (bad_count, S_components_dist, S_edges_dist, pentagon_overlap_dist)
def main(max_n=20, time_budget_per_n=1800):
print("Connectivity structure of S-vertices in bad colourings.\n")
grand_bad = 0
grand_comps = {}
grand_edges = {}
grand_overlap = {}
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_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}")
break
G.is_planar(set_embedding=True)
D = dual_of(G)
nb, sc, se, po = test_one(D)
n_bad_n += nb
for k, v in sc.items(): grand_comps[k] = grand_comps.get(k, 0) + v
for k, v in se.items(): grand_edges[k] = grand_edges.get(k, 0) + v
for k, v in po.items(): grand_overlap[k] = grand_overlap.get(k, 0) + v
elapsed = time.time() - start
print(f"n={n}: {n_bad_n} bad colourings [{elapsed:.0f}s]")
sys.stdout.flush()
grand_bad += n_bad_n
print()
print("=" * 70)
print(f"Total bad colourings: {grand_bad}")
print("\n(|S|, # connected components in H[S]) distribution:")
for k in sorted(grand_comps):
c = grand_comps[k]
print(f" |S|={k[0]}, #comps={k[1]}: {c}")
print("\n(|S|, # edges in H[S]) distribution:")
for k in sorted(grand_edges):
c = grand_edges[k]
print(f" |S|={k[0]}, #edges={k[1]}: {c}")
print("\n(|S|, max # shared pentagons across adjacent S-pairs):")
for k in sorted(grand_overlap):
c = grand_overlap[k]
print(f" |S|={k[0]}, max_overlap={k[1]}: {c}")
if __name__ == '__main__':
main()