1"""Stage 5: independent replay of every stored upper-bound witness and of the2P7 chronology, with a closure routine written from scratch (no import of3code/closure_oracle.py or code/graph_constructor.py).45Checks, per witness record in results/upper_bound_witnesses.jsonl:6 * the graph is P(n,5) rebuilt here from definition D1;7 * every stored force b -> w is legal at the moment it is applied8 (b black, w white, w the unique white neighbour of b);9 * the chronology ends with all 2n vertices black;10 * |S| equals the recorded size and the recorded Z upper bound in11 results/exact_values.csv;12 * independently, cl(S) = V by the from-scratch closure.13P7: for 12 <= n <= 300, generates the chronology exactly as written in the14proof of P7 (results/derivations.md) and replays it with the same legality15checker.16Output: results/robustness/witness_replay.json17"""18import csv19import json20import os21import sys2223ROOT = os.path.dirname(os.path.dirname(os.path.dirname(os.path.abspath(__file__))))24os.chdir(ROOT)252627def petersen(n, k):28 adj = {}29 for i in range(n):30 adj.setdefault(("u", i), set()).update({("u", (i + 1) % n), ("u", (i - 1) % n), ("v", i)})31 adj.setdefault(("v", i), set()).update({("v", (i + k) % n), ("v", (i - k) % n), ("u", i)})32 assert len(adj) == 2 * n and all(len(s) == 3 for s in adj.values())33 assert all(a in adj[b] for a in adj for b in adj[a])34 return adj353637def parse(label):38 return (label[0], int(label[1:]))394041def replay(adj, S, chronology):42 black = set(S)43 for src, tgt in chronology:44 b, w = parse(src), parse(tgt)45 if b not in black:46 return False, "source %s not black" % src47 if w in black:48 return False, "target %s already black" % tgt49 white = [x for x in adj[b] if x not in black]50 if white != [w] and set(white) != {w}:51 return False, "force %s->%s illegal: white nbrs %s" % (src, tgt, white)52 black.add(w)53 return len(black) == len(adj), "ended with %d black of %d" % (len(black), len(adj))545556def closure(adj, S):57 black = set(S)58 changed = True59 while changed:60 changed = False61 for b in list(black):62 white = [x for x in adj[b] if x not in black]63 if len(white) == 1:64 black.add(white[0])65 changed = True66 return black676869def p7_chronology(n):70 chron = []71 if n == 12:72 return [("u%d" % i, "v%d" % i) for i in range(12)]73 for i in range(1, 11):74 chron.append(("u%d" % i, "v%d" % i))75 chron.append(("v5", "v0"))76 chron.append(("v6", "v11"))77 for j in range(12, n):78 chron.append(("u%d" % (j - 1), "u%d" % j))79 chron.append(("v%d" % (j - 5), "v%d" % j))80 return chron818283def main():84 Z = {int(r["n"]): int(r["Z"]) for r in csv.DictReader(open("results/exact_values.csv"))}85 out = {"witnesses": [], "P7": []}86 allok = True87 for line in open("results/upper_bound_witnesses.jsonl"):88 r = json.loads(line)89 n, k = r["n"], r["k"]90 adj = petersen(n, k)91 S = [parse(x) for x in r["S"]]92 ok1, msg = replay(adj, S, r["chronology"]) if r.get("chronology") else (None, "no chronology stored")93 ok2 = closure(adj, S) == set(adj)94 # A valid forcing set smaller than the tabulated Z would refute the table; larger95 # witnesses (intermediate steps of the fort-cover descent) are legitimate.96 rec = {"n": n, "size": len(set(S)), "recorded_size": r.get("size"), "Z_table": Z.get(n), "chronology_ok": ok1,97 "chronology_msg": msg, "closure_ok": ok2, "size_matches_Z": len(set(S)) == Z.get(n),98 "size_below_Z_would_refute": len(set(S)) < Z.get(n), "source": r.get("source")}99 rec["ok"] = bool(ok2) and (ok1 is not False) and not rec["size_below_Z_would_refute"]100 allok &= rec["ok"]101 out["witnesses"].append(rec)102 out["n_with_size_Z_witness"] = sorted({w["n"] for w in out["witnesses"] if w["size_matches_Z"] and w["closure_ok"]})103 out["n_in_table_up_to_27_missing_size_Z_witness"] = [n for n in range(11, 28) if n not in out["n_with_size_Z_witness"] and Z.get(n) != 12]104 for n in range(12, 301):105 adj = petersen(n, 5)106 S = [("u", i) for i in range(12)]107 ok, msg = replay(adj, S, p7_chronology(n))108 out["P7"].append({"n": n, "ok": ok, "msg": msg})109 allok &= ok110 out["all_ok"] = allok111 out["num_witnesses"] = len(out["witnesses"])112 out["P7_range"] = [12, 300]113 json.dump(out, open("results/robustness/witness_replay.json", "w"), indent=1)114 print("witnesses:", len(out["witnesses"]), "all ok:", all(w["ok"] for w in out["witnesses"]))115 print("P7 chronology replays 12..300 all ok:", all(p["ok"] for p in out["P7"]))116 bad = [w for w in out["witnesses"] if not w["ok"]]117 for w in bad:118 print("BAD", w)119 return 0 if allok else 1120121122if __name__ == "__main__":123 sys.exit(main())124