didericis/math-research
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Save and verify explicit bridge-derived witnesses for the four duals

Browse Source 
The hunt only logged partition indices; the actual witness ELGs were lost.
Re-extract them (deterministic) with full bridge-switch paths and verify
every step independently. Saved as experiments/witnesses/dual_<i>.json
(labels, ELG source, ELG + dual graph6 and edge lists, the explicit
remove/add bridge-switch sequence, verified flag). All four verify:

  dual 0: ELG source 18, 3 bridge switches to dual
  dual 3: ELG source 16, 1 bridge switch  to dual
  dual 4: ELG source 20, 2 bridge switches to dual
  dual 5: ELG source  1, 4 bridge switches to dual

So each dual is only a handful of bridge switches from an Even Level Graph,
and the witnesses are now reproducible and human-checkable.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
This commit is contained in:
didericis
2026-05-22 11:00:16 -04:00
parent 30f28a60d6
commit 0c13758a2e
5 changed files with 2234 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
papers/even_level_graph_generators/experiments/extract_witnesses.py
+154
View File
@@ -0,0 +1,154 @@
"""Re-run the four known witness partitions, extract the actual witness
Even Level Graph and the bridge-switch path ELG -> dual, verify every
step, and save to experiments/witnesses/dual_<i>.json so the result is
reproducible and independently checkable.
"""
import sys
import os
import json
sys.path.insert(0, '/Users/didericis/Code/math-research/papers/'
'level_resolutions_of_maximal_planar_graphs/experiments')
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import networkx as nx
from load_holton_mckay import parse_planar_code
from tutte_dual_treecolor import dual_triangulation
from exhaustive_bridge import valid_parity_partitions
from fast_bridge import EdgeCode, parity_bridges
from fast_decide import expand_and_check
from test_conjecture import is_even_level_graph
# dual index -> witness partition index (from the hunt logs)
WITNESS_PARTITION = {0: 12, 3: 9, 4: 23, 5: 12}
def forward_bridge_states(state, code, labels):
"""Yield (neighbor_state, removed_edge, added_edge) for each forward
bridge switch from `state`."""
G = code.graph_of(state)
ok, emb = nx.check_planarity(G)
if not ok:
return
for u, v in list(G.edges()):
if labels[u] != labels[v]:
continue # only flip same-parity edges
f1 = emb.traverse_face(u, v)
if len(f1) != 3:
continue
f2 = emb.traverse_face(v, u)
if len(f2) != 3:
continue
w = next(a for a in f1 if a != u and a != v)
x = next(b for b in f2 if b != u and b != v)
if w == x or G.has_edge(w, x):
continue
Gp = G.copy(); Gp.remove_edge(u, v); Gp.add_edge(w, x)
# bridge condition on the new edge wx in the post-state Gp:
if labels[w] == labels[x]:
ev = {a: set() for a in code.nodes if labels[a] == labels[w]}
for a, b in Gp.edges():
if labels[a] == labels[w] and labels[b] == labels[w]:
ev[a].add(b); ev[b].add(a)
if frozenset((w, x)) not in parity_bridges(ev):
continue
ns = (state & ~(1 << code.bit(u, v))) | (1 << code.bit(w, x))
yield ns, (u, v), (w, x)
def find_witness_path(code, labels, n, cap=4_000_000):
"""Backward BFS with parent pointers from the dual; return (witness
state, path of states ELG..dual) or None."""
s0 = code.state0
parent = {s0: None}
frontier = [s0]
while frontier and len(parent) < cap:
new = []
for st in frontier:
wit, neigh = expand_and_check(st, code, labels, n)
if wit:
# reconstruct ELG=st -> ... -> dual via parents
path = []
cur = st
while cur is not None:
path.append(cur)
cur = parent[cur]
return st, path # path[0]=ELG ... path[-1]=dual
for ns in neigh:
if ns not in parent:
parent[ns] = st
new.append(ns)
frontier = new
return None, None
def verify_path(code, labels, path, n):
"""Verify path[0] is an ELG matching labels, and each consecutive pair
is a forward bridge switch. Returns (ok, source, steps)."""
# ELG check
G0 = code.graph_of(path[0])
src = None
for s in code.nodes:
ok, lvls = is_even_level_graph(G0, frozenset({s}))
if ok and all((lvls[v] % 2 == 0) == (labels[v] == labels[s])
for v in code.nodes):
src = s
break
if src is None:
return False, None, None
steps = []
for a, b in zip(path, path[1:]):
match = None
for ns, rem, add in forward_bridge_states(a, code, labels):
if ns == b:
match = (rem, add)
break
if match is None:
return False, src, None
steps.append(match)
return True, src, steps
def main():
outdir = os.path.join(os.path.dirname(os.path.abspath(__file__)),
'witnesses')
os.makedirs(outdir, exist_ok=True)
graphs = parse_planar_code('experiments/nonham38m4.pc')
for i, p in WITNESS_PARTITION.items():
G, _ = dual_triangulation(graphs[i][0])
n = G.number_of_nodes()
code = EdgeCode(G.nodes())
code.state0 = code.state_of(G)
labels = list(valid_parity_partitions(G))[p]
wit, path = find_witness_path(code, labels, n)
if wit is None:
print(f'dual {i}: NO witness found at partition {p} (?)', flush=True)
continue
ok, src, steps = verify_path(code, labels, path, n)
elg_edges = sorted(tuple(sorted(e)) for e in code.edges_of(path[0]))
dual_edges = sorted(tuple(sorted(e)) for e in code.edges_of(path[-1]))
data = {
'dual_index': i,
'n': n,
'partition_index': p,
'labels': {str(v): labels[v] for v in code.nodes},
'elg_source': src,
'elg_graph6': nx.to_graph6_bytes(
code.graph_of(path[0]), header=False).decode().strip(),
'dual_graph6': nx.to_graph6_bytes(
code.graph_of(path[-1]), header=False).decode().strip(),
'elg_edges': elg_edges,
'dual_edges': dual_edges,
'num_bridge_switches': len(path) - 1,
'bridge_switches': [
{'remove': list(r), 'add': list(a)} for r, a in (steps or [])
],
'verified': bool(ok),
}
with open(os.path.join(outdir, f'dual_{i}.json'), 'w') as fh:
json.dump(data, fh, indent=2)
print(f'dual {i}: witness ELG (source {src}), '
f'{len(path)-1} bridge switches to dual, verified={ok}',
flush=True)
if __name__ == '__main__':
main()
papers/even_level_graph_generators/experiments/witnesses/dual_0.json
+525
View File
@@ -0,0 +1,525 @@
{
"dual_index": 0,
"n": 21,
"partition_index": 12,
"labels": {
"0": 0,
"1": 1,
"2": 1,
"3": 1,
"4": 0,
"5": 0,
"6": 0,
"7": 1,
"8": 0,
"9": 1,
"10": 1,
"11": 1,
"12": 1,
"13": 0,
"14": 0,
"15": 0,
"16": 1,
"17": 1,
"18": 1,
"19": 0,
"20": 0
},
"elg_source": 18,
"elg_graph6": "T}HiloZBgP@B?M?F_@O?E??g?Hg?A_?Cs?@N",
"dual_graph6": "T}hikoZBgP@B?M?F_@O?E??g?H_?Ag?Cs??n",
"elg_edges": [
[
0,
1
],
[
0,
2
],
[
0,
3
],
[
0,
7
],
[
1,
2
],
[
1,
3
],
[
1,
5
],
[
1,
6
],
[
2,
4
],
[
2,
5
],
[
2,
7
],
[
3,
6
],
[
3,
7
],
[
3,
8
],
[
4,
5
],
[
4,
7
],
[
4,
8
],
[
4,
9
],
[
4,
10
],
[
4,
11
],
[
5,
6
],
[
5,
9
],
[
6,
8
],
[
6,
9
],
[
7,
8
],
[
8,
9
],
[
8,
10
],
[
8,
12
],
[
9,
11
],
[
9,
12
],
[
9,
13
],
[
10,
11
],
[
10,
12
],
[
10,
13
],
[
10,
14
],
[
10,
17
],
[
11,
13
],
[
12,
13
],
[
12,
14
],
[
12,
15
],
[
12,
16
],
[
12,
19
],
[
13,
15
],
[
13,
17
],
[
13,
18
],
[
13,
20
],
[
14,
16
],
[
14,
17
],
[
15,
18
],
[
15,
19
],
[
16,
17
],
[
16,
19
],
[
16,
20
],
[
17,
20
],
[
18,
19
],
[
18,
20
],
[
19,
20
]
],
"dual_edges": [
[
0,
1
],
[
0,
2
],
[
0,
3
],
[
0,
4
],
[
0,
7
],
[
1,
2
],
[
1,
3
],
[
1,
5
],
[
1,
6
],
[
2,
4
],
[
2,
5
],
[
3,
6
],
[
3,
7
],
[
3,
8
],
[
4,
5
],
[
4,
7
],
[
4,
8
],
[
4,
9
],
[
4,
10
],
[
4,
11
],
[
5,
6
],
[
5,
9
],
[
6,
8
],
[
6,
9
],
[
7,
8
],
[
8,
9
],
[
8,
10
],
[
8,
12
],
[
9,
11
],
[
9,
12
],
[
9,
13
],
[
10,
11
],
[
10,
12
],
[
10,
13
],
[
10,
14
],
[
10,
17
],
[
11,
13
],
[
12,
13
],
[
12,
14
],
[
12,
15
],
[
12,
16
],
[
12,
19
],
[
13,
15
],
[
13,
17
],
[
13,
18
],
[
14,
16
],
[
14,
17
],
[
14,
20
],
[
15,
18
],
[
15,
19
],
[
16,
19
],
[
16,
20
],
[
17,
18
],
[
17,
20
],
[
18,
19
],
[
18,
20
],
[
19,
20
]
],
"num_bridge_switches": 3,
"bridge_switches": [
{
"remove": [
13,
20
],
"add": [
18,
17
]
},
{
"remove": [
16,
17
],
"add": [
14,
20
]
},
{
"remove": [
2,
7
],
"add": [
4,
0
]
}
],
"verified": true
}
papers/even_level_graph_generators/experiments/witnesses/dual_3.json
+505
View File
@@ -0,0 +1,505 @@
{
"dual_index": 3,
"n": 21,
"partition_index": 9,
"labels": {
"0": 0,
"1": 1,
"2": 0,
"3": 0,
"4": 1,
"5": 1,
"6": 0,
"7": 0,
"8": 1,
"9": 1,
"10": 0,
"11": 0,
"12": 0,
"13": 0,
"14": 0,
"15": 1,
"16": 1,
"17": 1,
"18": 1,
"19": 0,
"20": 0
},
"elg_source": 16,
"elg_graph6": "T}lahWYE?^AEAK?L?AO?b??g?b??Ag?@s?AN",
"dual_graph6": "T}lahWYE?^AEAK?L_AO?b??g?B??Ag?@s?AN",
"elg_edges": [
[
0,
1
],
[
0,
2
],
[
0,
3
],
[
0,
4
],
[
1,
2
],
[
1,
3
],
[
1,
5
],
[
1,
6
],
[
2,
4
],
[
2,
5
],
[
2,
7
],
[
3,
4
],
[
3,
6
],
[
3,
8
],
[
3,
9
],
[
3,
11
],
[
4,
7
],
[
4,
8
],
[
4,
9
],
[
4,
10
],
[
4,
12
],
[
5,
6
],
[
5,
7
],
[
5,
10
],
[
6,
8
],
[
6,
10
],
[
7,
10
],
[
8,
10
],
[
8,
11
],
[
8,
12
],
[
8,
13
],
[
8,
17
],
[
9,
11
],
[
9,
12
],
[
9,
13
],
[
9,
14
],
[
9,
15
],
[
11,
13
],
[
12,
14
],
[
12,
16
],
[
12,
17
],
[
12,
20
],
[
13,
15
],
[
13,
17
],
[
13,
18
],
[
14,
15
],
[
14,
16
],
[
14,
19
],
[
15,
18
],
[
15,
19
],
[
16,
19
],
[
16,
20
],
[
17,
18
],
[
17,
20
],
[
18,
19
],
[
18,
20
],
[
19,
20
]
],
"dual_edges": [
[
0,
1
],
[
0,
2
],
[
0,
3
],
[
0,
4
],
[
1,
2
],
[
1,
3
],
[
1,
5
],
[
1,
6
],
[
2,
4
],
[
2,
5
],
[
2,
7
],
[
3,
4
],
[
3,
6
],
[
3,
8
],
[
3,
9
],
[
3,
11
],
[
4,
7
],
[
4,
8
],
[
4,
9
],
[
4,
10
],
[
4,
12
],
[
5,
6
],
[
5,
7
],
[
5,
10
],
[
6,
8
],
[
6,
10
],
[
7,
10
],
[
8,
10
],
[
8,
11
],
[
8,
12
],
[
8,
13
],
[
9,
11
],
[
9,
12
],
[
9,
13
],
[
9,
14
],
[
9,
15
],
[
11,
13
],
[
12,
13
],
[
12,
14
],
[
12,
16
],
[
12,
17
],
[
12,
20
],
[
13,
15
],
[
13,
17
],
[
13,
18
],
[
14,
15
],
[
14,
16
],
[
14,
19
],
[
15,
18
],
[
15,
19
],
[
16,
19
],
[
16,
20
],
[
17,
18
],
[
17,
20
],
[
18,
19
],
[
18,
20
],
[
19,
20
]
],
"num_bridge_switches": 1,
"bridge_switches": [
{
"remove": [
8,
17
],
"add": [
13,
12
]
}
],
"verified": true
}
papers/even_level_graph_generators/experiments/witnesses/dual_4.json
+515
View File
@@ -0,0 +1,515 @@
{
"dual_index": 4,
"n": 21,
"partition_index": 23,
"labels": {
"0": 0,
"1": 1,
"2": 1,
"3": 1,
"4": 1,
"5": 0,
"6": 0,
"7": 0,
"8": 0,
"9": 0,
"10": 1,
"11": 1,
"12": 1,
"13": 1,
"14": 1,
"15": 0,
"16": 1,
"17": 1,
"18": 0,
"19": 1,
"20": 0
},
"elg_source": 20,
"elg_graph6": "T}halaGIXIAW_[_G?xc?E?G??AW@Aw@CO?AL",
"dual_graph6": "T}halaGIXIAW_[_G?xc?E?GO?AO?Aw@CO?AN",
"elg_edges": [
[
0,
1
],
[
0,
2
],
[
0,
3
],
[
0,
4
],
[
0,
7
],
[
0,
8
],
[
0,
12
],
[
0,
13
],
[
0,
15
],
[
1,
2
],
[
1,
3
],
[
1,
5
],
[
1,
6
],
[
2,
4
],
[
2,
5
],
[
2,
7
],
[
2,
9
],
[
2,
10
],
[
3,
6
],
[
3,
7
],
[
3,
11
],
[
4,
8
],
[
4,
9
],
[
5,
6
],
[
5,
10
],
[
5,
14
],
[
6,
11
],
[
6,
14
],
[
7,
9
],
[
7,
10
],
[
7,
11
],
[
7,
12
],
[
7,
14
],
[
8,
9
],
[
8,
12
],
[
8,
13
],
[
8,
16
],
[
8,
18
],
[
8,
19
],
[
9,
12
],
[
10,
14
],
[
11,
14
],
[
12,
15
],
[
12,
17
],
[
12,
19
],
[
12,
20
],
[
13,
15
],
[
13,
18
],
[
15,
17
],
[
15,
18
],
[
16,
17
],
[
16,
18
],
[
16,
19
],
[
16,
20
],
[
17,
18
],
[
17,
20
],
[
19,
20
]
],
"dual_edges": [
[
0,
1
],
[
0,
2
],
[
0,
3
],
[
0,
4
],
[
0,
7
],
[
0,
8
],
[
0,
12
],
[
0,
13
],
[
0,
15
],
[
1,
2
],
[
1,
3
],
[
1,
5
],
[
1,
6
],
[
2,
4
],
[
2,
5
],
[
2,
7
],
[
2,
9
],
[
2,
10
],
[
3,
6
],
[
3,
7
],
[
3,
11
],
[
4,
8
],
[
4,
9
],
[
5,
6
],
[
5,
10
],
[
5,
14
],
[
6,
11
],
[
6,
14
],
[
7,
9
],
[
7,
10
],
[
7,
11
],
[
7,
12
],
[
7,
14
],
[
8,
9
],
[
8,
12
],
[
8,
13
],
[
8,
16
],
[
8,
19
],
[
9,
12
],
[
10,
14
],
[
11,
14
],
[
12,
15
],
[
12,
17
],
[
12,
19
],
[
12,
20
],
[
13,
15
],
[
13,
16
],
[
13,
18
],
[
15,
17
],
[
15,
18
],
[
16,
18
],
[
16,
19
],
[
16,
20
],
[
17,
18
],
[
17,
20
],
[
18,
20
],
[
19,
20
]
],
"num_bridge_switches": 2,
"bridge_switches": [
{
"remove": [
16,
17
],
"add": [
20,
18
]
},
{
"remove": [
8,
18
],
"add": [
16,
13
]
}
],
"verified": true
}
papers/even_level_graph_generators/experiments/witnesses/dual_5.json
+535
View File
@@ -0,0 +1,535 @@
{
"dual_index": 5,
"n": 21,
"partition_index": 12,
"labels": {
"0": 0,
"1": 1,
"2": 0,
"3": 0,
"4": 1,
"5": 1,
"6": 0,
"7": 1,
"8": 1,
"9": 0,
"10": 1,
"11": 1,
"12": 1,
"13": 1,
"14": 0,
"15": 1,
"16": 0,
"17": 0,
"18": 0,
"19": 1,
"20": 0
},
"elg_source": 1,
"elg_graph6": "T}gblqGAXIAw_[_G?hc?E?GO?AO?Aw??[?aL",
"dual_graph6": "T}halaGIXIAW_[_G?xc?E?GO?AO?Aw@?[?aD",
"elg_edges": [
[
0,
1
],
[
0,
2
],
[
0,
3
],
[
0,
4
],
[
0,
7
],
[
0,
8
],
[
0,
12
],
[
0,
13
],
[
0,
15
],
[
1,
2
],
[
1,
3
],
[
1,
6
],
[
2,
4
],
[
2,
5
],
[
2,
6
],
[
2,
7
],
[
2,
10
],
[
3,
6
],
[
3,
7
],
[
3,
11
],
[
4,
7
],
[
4,
8
],
[
4,
9
],
[
5,
6
],
[
5,
10
],
[
5,
11
],
[
5,
14
],
[
6,
11
],
[
7,
9
],
[
7,
10
],
[
7,
11
],
[
7,
12
],
[
7,
14
],
[
8,
9
],
[
8,
12
],
[
8,
13
],
[
8,
16
],
[
8,
20
],
[
9,
12
],
[
10,
14
],
[
11,
14
],
[
12,
15
],
[
12,
17
],
[
12,
20
],
[
13,
15
],
[
13,
16
],
[
13,
18
],
[
15,
17
],
[
15,
18
],
[
16,
18
],
[
16,
19
],
[
16,
20
],
[
17,
18
],
[
17,
19
],
[
17,
20
],
[
18,
19
],
[
19,
20
]
],
"dual_edges": [
[
0,
1
],
[
0,
2
],
[
0,
3
],
[
0,
4
],
[
0,
7
],
[
0,
8
],
[
0,
12
],
[
0,
13
],
[
0,
15
],
[
1,
2
],
[
1,
3
],
[
1,
5
],
[
1,
6
],
[
2,
4
],
[
2,
5
],
[
2,
7
],
[
2,
9
],
[
2,
10
],
[
3,
6
],
[
3,
7
],
[
3,
11
],
[
4,
8
],
[
4,
9
],
[
5,
6
],
[
5,
10
],
[
5,
14
],
[
6,
11
],
[
6,
14
],
[
7,
9
],
[
7,
10
],
[
7,
11
],
[
7,
12
],
[
7,
14
],
[
8,
9
],
[
8,
12
],
[
8,
13
],
[
8,
16
],
[
8,
19
],
[
8,
20
],
[
9,
12
],
[
10,
14
],
[
11,
14
],
[
12,
15
],
[
12,
17
],
[
12,
20
],
[
13,
15
],
[
13,
16
],
[
13,
18
],
[
15,
17
],
[
15,
18
],
[
16,
18
],
[
16,
19
],
[
17,
18
],
[
17,
19
],
[
17,
20
],
[
18,
19
],
[
19,
20
]
],
"num_bridge_switches": 4,
"bridge_switches": [
{
"remove": [
16,
20
],
"add": [
8,
19
]
},
{
"remove": [
5,
11
],
"add": [
6,
14
]
},
{
"remove": [
4,
7
],
"add": [
2,
9
]
},
{
"remove": [
2,
6
],
"add": [
1,
5
]
}
],
"verified": true
}