face_monochromatic_pairs: empirical near-proof of Conjecture 5.1 via Lemma 5.3

Add Remark 5.5 immediately after Lemma 5.3's proof, recording the
empirical reduction of Conjecture 5.1 via the contrapositive of
Lemma 5.3: the conjecture follows from "h_phi is not constant on
V(K_b) U V(K_c)", and we have verified that non-constancy holds on
every one of 142,812 chord-apex+Kempe colourings up to n <= 20
(including the six Holton-McKay duals as a special case).

This is an independent empirical near-proof of Conjecture 5.1,
complementary to the direct (1)-(3) witness check in
Remark 5.6 / rem:conj-3-6-empirical. A structural proof of the
non-constancy claim would upgrade this to a proof of the
conjecture.

Also include two diagnostic scripts that informed the remark:
  - check_shared_parity.py: parity-bucket symmetry n_{0,0} = n_{1,1},
    n_{0,1} = n_{1,0} at vertices in V(K_b) cap V(K_c). 100%.
  - check_cw_parity_prediction.py: structural identity
    s_b XOR s_c = i_b XOR i_c XOR 1 holds at every shared vertex
    (263,004 / 263,004), and the simple constancy prediction matches
    exactly 50% of shared vertices per colouring with 0 perfectly
    matching colourings.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
This commit is contained in:
2026-05-25 00:21:52 -04:00
parent d659bf40d5
commit 703b523161
6 changed files with 476 additions and 40 deletions
@@ -0,0 +1,212 @@
"""Test the CW-order-forced parity relation at each shared vertex.
At each v in V(K_b) cap V(K_c), under the constancy hypothesis h(v) = +1
(CW colour order (a, b, c) at v), Lemma A predicts:
s_b(v) = i_b(v) mod 2 # side of c-edge relative to K_b walk
s_c(v) = (i_c(v) + 1) mod 2 # side of b-edge relative to K_c walk
The actual sides are determined by the embedding and the actual h(v).
The formulas combine to (regardless of h(v)):
s_b(v) XOR s_c(v) = (i_b(v) XOR i_c(v) XOR 1) mod 2
which is a structural identity. We verify this identity and tally the
joint (h, i_b mod 2, i_c mod 2, s_b, s_c) over all shared vertices.
Most informative: under the constancy hypothesis (h(v) = +1 fixed), the
formulas s_b = i_b and s_c = 1 XOR i_c are the prediction. We check at
each shared v whether the actual (s_b, s_c) matches this prediction --
and where the mismatches occur. Mismatches signal Heawood h(v) = -1 at v.
Run with: sage experiments/check_cw_parity_prediction.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,
trace_kempe_cycle,
edge_idx,
)
from check_heawood_on_kempe import dual_of, heawood_numbers
from check_heawood_local_side import c_edge_local_side
def walk_positions(walk):
pos = {}
for k, (_, leave_v) in enumerate(walk):
if leave_v not in pos:
pos[leave_v] = k
return pos
def test_one(D):
D.is_planar(set_embedding=True)
n_col = 0
# For each shared vertex: record (h_b, i_b mod 2, i_c mod 2, s_b, s_c).
joint = {}
# Verify the identity s_b XOR s_c == (i_b XOR i_c XOR 1) for each
# shared v.
identity_holds = 0; identity_fails = 0
# Under constancy h = +1 prediction: predict s_b = i_b, s_c = 1 XOR i_c.
# Count how often the prediction matches per-vertex.
constancy_matches = 0
constancy_total = 0
# Per-colouring: count #shared v where constancy prediction matches.
constancy_dist = {} # # of shared v matching -> #colourings
constancy_perfect = 0 # #colourings where prediction matches at all v
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)
emb = H.get_embedding()
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
try:
h = heawood_numbers(H, edges, col)
except RuntimeError:
continue
merged_idx = edge_idx(edges, named['merged'])
a = col[merged_idx]
bs = [c for c in range(3) if c != a]
b_color, c_color = bs[0], bs[1]
# The "third colour" at each cycle.
walk_b = trace_kempe_cycle(edges, col, merged_idx, (a, b_color))
walk_c = trace_kempe_cycle(edges, col, merged_idx, (a, c_color))
pos_b = walk_positions(walk_b)
pos_c = walk_positions(walk_c)
V_b = set(pos_b.keys())
V_c = set(pos_c.keys())
shared = V_b & V_c
# Compute s_b for each v on K_b
Lb = len(walk_b)
sides_b = {}
for k in range(Lb):
v = walk_b[k][1]
in_e = edges[walk_b[k][0]]
out_e = edges[walk_b[(k+1) % Lb][0]]
u_in = in_e[0] if in_e[1] == v else in_e[1]
u_out = out_e[0] if out_e[1] == v else out_e[1]
s = c_edge_local_side(v, c_color, col, edges, emb,
u_in, u_out)
sides_b[v] = (0 if s == 'L' else 1) if s else None
# Compute s_c for each v on K_c. "Third colour off K_c" = b_color.
Lc = len(walk_c)
sides_c = {}
for k in range(Lc):
v = walk_c[k][1]
in_e = edges[walk_c[k][0]]
out_e = edges[walk_c[(k+1) % Lc][0]]
u_in = in_e[0] if in_e[1] == v else in_e[1]
u_out = out_e[0] if out_e[1] == v else out_e[1]
s = c_edge_local_side(v, b_color, col, edges, emb,
u_in, u_out)
sides_c[v] = (0 if s == 'L' else 1) if s else None
# For each shared v, record.
col_matches = 0
col_shared_count = 0
for v in shared:
pb = pos_b[v] % 2
pc = pos_c[v] % 2
sb = sides_b.get(v)
sc = sides_c.get(v)
hv = h[v]
h_b = 1 if hv == 1 else 0
if sb is None or sc is None: continue
key = (h_b, pb, pc, sb, sc)
joint[key] = joint.get(key, 0) + 1
# Identity check: s_b XOR s_c == (i_b XOR i_c XOR 1)
if (sb ^ sc) == (pb ^ pc ^ 1):
identity_holds += 1
else:
identity_fails += 1
# Constancy prediction: s_b = i_b, s_c = 1 XOR i_c
pred_match = (sb == pb) and (sc == (1 - pc))
constancy_total += 1
col_shared_count += 1
if pred_match:
constancy_matches += 1
col_matches += 1
if col_shared_count > 0:
constancy_dist[(col_matches, col_shared_count)] = \
constancy_dist.get(
(col_matches, col_shared_count), 0) + 1
if col_matches == col_shared_count:
constancy_perfect += 1
return (n_col, joint, identity_holds, identity_fails,
constancy_matches, constancy_total,
constancy_dist, constancy_perfect)
def main(max_n=18, time_budget_per_n=1800):
print(f"CW-parity prediction at shared K_b cap K_c, n in [12, {max_n}]\n")
grand_col = 0
grand_joint = {}
grand_id_ok = 0; grand_id_fail = 0
grand_cm = 0; grand_ct = 0
grand_cd = {}
grand_cp = 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
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, ji, ido, idf, cm, ct,
cd, cp) = test_one(D)
n_col_n += ni
for k, v in ji.items(): grand_joint[k] = grand_joint.get(k, 0) + v
grand_id_ok += ido; grand_id_fail += idf
grand_cm += cm; grand_ct += ct
for k, v in cd.items(): grand_cd[k] = grand_cd.get(k, 0) + v
grand_cp += cp
elapsed = time.time() - start
print(f"n={n}: {n_col_n} col., [{elapsed:.0f}s]")
sys.stdout.flush()
grand_col += n_col_n
print()
print("=" * 78)
print(f"Grand totals (n in [12, {max_n}], {grand_col} colourings)")
print(f"\n Structural identity s_b XOR s_c == i_b XOR i_c XOR 1:")
print(f" holds: {grand_id_ok}, fails: {grand_id_fail}")
print(f"\n Constancy prediction (s_b == i_b mod 2 AND s_c == 1 - i_c mod 2)")
print(f" match rate per shared vertex: "
f"{grand_cm}/{grand_ct} ({100*grand_cm/max(1,grand_ct):.2f}%)")
print(f" perfect (all shared v match) colourings: "
f"{grand_cp}/{grand_col} ({100*grand_cp/max(1,grand_col):.2f}%)")
print(f"\n Joint (h_b, i_b mod 2, i_c mod 2, s_b, s_c) distribution:")
keys = sorted(grand_joint.keys())
total = sum(grand_joint.values())
# Group by (h_b, i_b mod 2, i_c mod 2) and show s_b, s_c spread:
for k in keys:
v = grand_joint[k]
print(f" {k}: {v} ({100*v/max(1,total):.2f}%)")
if __name__ == '__main__':
main()
@@ -0,0 +1,180 @@
"""For each chord-apex+Kempe colouring, walk K_b and K_c (each in
trace order starting from the merged edge), and for every shared
vertex v in V(K_b) cap V(K_c) record:
i_b(v) = position of v in the K_b walk (mod 2)
i_c(v) = position of v in the K_c walk (mod 2)
h_phi(v)
The proposal: under the constant-Heawood hypothesis, Lemma A forces
each cycle's c-edge / b-edge sides to be determined by i mod 2. The
CW order at a shared vertex v relates these. We tally the joint
distribution of (i_b mod 2, i_c mod 2, h(v)) across all colourings
and shared vertices, looking for a parity constraint.
Run with: sage experiments/check_shared_parity.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,
trace_kempe_cycle,
edge_idx,
)
from check_heawood_on_kempe import dual_of, heawood_numbers
def walk_positions(walk):
"""Return dict vertex -> first-position-on-walk."""
pos = {}
for k, (_, leave_v) in enumerate(walk):
if leave_v not in pos:
pos[leave_v] = k
return pos
def test_one(D):
D.is_planar(set_embedding=True)
n_col = 0
# Joint distribution: (i_b mod 2, i_c mod 2, h) -> count
joint = {}
# Per-colouring: count of shared vertices in each of the 4
# (i_b, i_c) parity buckets, summarised.
bucket_dist = {} # (n00, n01, n10, n11) -> count
# Per-colouring: is sum of i_b parities over shared vertices ==
# sum of i_c parities (mod 2)?
sum_parity_match = 0
sum_parity_total = 0
# Per-colouring: is i_b(v) congruent to i_c(v) (mod 2) for ALL
# shared vertices? Or NEVER? Or mixed?
all_match = 0
all_diff = 0
mixed = 0
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
try:
h = heawood_numbers(H, edges, col)
except RuntimeError:
continue
merged_idx = edge_idx(edges, named['merged'])
a = col[merged_idx]
bs = [c for c in range(3) if c != a]
walk_b = trace_kempe_cycle(edges, col, merged_idx, (a, bs[0]))
walk_c = trace_kempe_cycle(edges, col, merged_idx, (a, bs[1]))
pos_b = walk_positions(walk_b)
pos_c = walk_positions(walk_c)
V_b = set(pos_b.keys())
V_c = set(pos_c.keys())
shared = V_b & V_c
buckets = [0, 0, 0, 0] # (i_b, i_c) parities
sum_ib = 0
sum_ic = 0
match_count = 0
diff_count = 0
for v in shared:
pb = pos_b[v] % 2
pc = pos_c[v] % 2
buckets[2 * pb + pc] += 1
sum_ib = (sum_ib + pb) % 2
sum_ic = (sum_ic + pc) % 2
key = (pb, pc, h[v])
joint[key] = joint.get(key, 0) + 1
if pb == pc: match_count += 1
else: diff_count += 1
if shared:
sum_parity_total += 1
if sum_ib == sum_ic:
sum_parity_match += 1
if diff_count == 0:
all_match += 1
elif match_count == 0:
all_diff += 1
else:
mixed += 1
bd_key = tuple(buckets)
bucket_dist[bd_key] = bucket_dist.get(bd_key, 0) + 1
return n_col, joint, bucket_dist, sum_parity_match, sum_parity_total, all_match, all_diff, mixed
def main(max_n=18, time_budget_per_n=1800):
print(f"Parity check at shared K_b cap K_c vertices, "
f"n in [12, {max_n}]\n")
grand_col = 0
grand_joint = {}
grand_bucket = {}
grand_spm = 0; grand_spt = 0
grand_am = 0; grand_ad = 0; grand_mix = 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
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)
(n_col_i, j_i, b_i, spm_i, spt_i,
am_i, ad_i, mix_i) = test_one(D)
n_col_n += n_col_i
for k, v in j_i.items(): grand_joint[k] = grand_joint.get(k, 0) + v
for k, v in b_i.items(): grand_bucket[k] = grand_bucket.get(k, 0) + v
grand_spm += spm_i; grand_spt += spt_i
grand_am += am_i; grand_ad += ad_i; grand_mix += mix_i
elapsed = time.time() - start
print(f"n={n}: {n_col_n} col., [{elapsed:.0f}s]")
sys.stdout.flush()
grand_col += n_col_n
print()
print("=" * 78)
print(f"Grand totals (n in [12, {max_n}], {grand_col} colourings):")
print(f"\n Joint (i_b mod 2, i_c mod 2, h_phi) distribution over "
f"shared vertices:")
keys = sorted(grand_joint.keys())
total_shared = sum(grand_joint.values())
for k in keys:
v = grand_joint[k]
print(f" {k}: {v} ({100*v/max(1,total_shared):.2f}%)")
print(f"\n Per-colouring: i_b(v) == i_c(v) (mod 2) for ALL shared v?")
print(f" all match: {grand_am}/{grand_col} "
f"({100*grand_am/max(1,grand_col):.2f}%)")
print(f" all differ: {grand_ad}/{grand_col} "
f"({100*grand_ad/max(1,grand_col):.2f}%)")
print(f" mixed: {grand_mix}/{grand_col} "
f"({100*grand_mix/max(1,grand_col):.2f}%)")
print(f"\n Per-colouring: sum_{{v shared}} i_b(v) ≡ sum_{{v shared}} i_c(v) (mod 2)?")
print(f" sum-parity match: {grand_spm}/{grand_spt} "
f"({100*grand_spm/max(1,grand_spt):.2f}%)")
print(f"\n Most common bucket signatures (n00, n01, n10, n11):")
bs = sorted(grand_bucket.items(), key=lambda kv: -kv[1])[:8]
for k, v in bs:
print(f" {k}: {v} ({100*v/max(1,grand_col):.2f}%)")
if __name__ == '__main__':
main()