1"""Independent upper-bound checker. Imports nothing from the solver or oracle2modules: it rebuilds P(n,5) from the definition, replays every stored3chronology in results/upper_bound_witnesses.jsonl force by force (checking4that the source is black, the target white, and the target is the unique5white neighbour of the source), and checks that the final set is V.6Also replays the uniform 12-vertex construction of P7 for 13 <= n <= NMAX.7Writes results/upper_bound_verification.json. Exit code 1 on any failure.8"""9import json10import os11import sys1213ROOT = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))14os.chdir(ROOT)151617def petersen_adj(n, k):18 adj = {}19 for i in range(n):20 for a, b in ((("u", i), ("u", (i + 1) % n)), (("u", i), ("v", i)), (("v", i), ("v", (i + k) % n))):21 adj.setdefault(a, set()).add(b)22 adj.setdefault(b, set()).add(a)23 return adj242526def parse(lbl):27 return (lbl[0], int(lbl[1:]))282930def replay(adj, S, chron):31 black = set(S)32 for idx, (b, w) in enumerate(chron):33 if b not in black or w in black:34 return False, idx35 white = [x for x in adj[b] if x not in black]36 if white != [w]:37 return False, idx38 black.add(w)39 return len(black) == len(adj), None404142def p7_chronology(n):43 S = [("u", i) for i in range(12)]44 ch = [(("u", i), ("v", i)) for i in range(1, 11)] + [(("v", 5), ("v", 0)), (("v", 6), ("v", 11))]45 for j in range(12, n):46 ch.append((("u", j - 1), ("u", j)))47 ch.append((("v", j - 5), ("v", j)))48 return S, ch495051if __name__ == "__main__":52 nmax = int(sys.argv[1]) if len(sys.argv) > 1 else 6053 report = {"witnesses": [], "P7": []}54 ok_all = True55 path = "results/upper_bound_witnesses.jsonl"56 seen = set()57 if os.path.exists(path):58 for line in open(path):59 w = json.loads(line)60 n = w["n"]61 adj = petersen_adj(n, w["k"])62 S = [parse(s) for s in w["S"]]63 chron = [(parse(a), parse(b)) for a, b in w["chronology"]]64 ok, bad = replay(adj, S, chron)65 ok = ok and len(set(S)) == w["size"] == len(S)66 report["witnesses"].append({"n": n, "size": w["size"], "replay_ok": ok, "first_bad_force": bad, "source": w.get("source")})67 ok_all &= ok68 for n in range(13, nmax + 1):69 adj = petersen_adj(n, 5)70 S, ch = p7_chronology(n)71 ok, bad = replay(adj, S, ch)72 report["P7"].append({"n": n, "replay_ok": ok, "forces": len(ch)})73 ok_all &= ok74 # n = 12: outer layer then spokes75 adj = petersen_adj(12, 5)76 ok, bad = replay(adj, [("u", i) for i in range(12)], [(("u", i), ("v", i)) for i in range(12)])77 report["P7"].insert(0, {"n": 12, "replay_ok": ok, "forces": 12})78 ok_all &= ok79 report["all_ok"] = ok_all80 with open("results/upper_bound_verification.json", "w") as f:81 json.dump(report, f, indent=1)82 print("witness replays: %d, P7 replays: %d, all ok: %s" % (len(report["witnesses"]), len(report["P7"]), ok_all))83 sys.exit(0 if ok_all else 1)84