1"""Merges all evidence into the value tables and metrics:2 results/exact_values.csv n, Z, upper evidence, lower evidence, status3 results/known_vs_new.csv literature status per n4 results/tables/*.csv manuscript tables5 results/metrics.json headline numbers6Evidence sources: results/brute_force_values.json (exhaustive, C oracle),7results/upper_bound_witnesses.jsonl, results/lower_bound_certificates.jsonl8(fort cover, DRAT checked), results/boundary_certificates.jsonl (DRAT checked;9with Lemma 3.1 gives Z >= 12 when n >= ceil((p+11)/2)), results/solver_runs.jsonl,10results/upper_bound_verification.json, results/lower_bound_verification.json.11Status rule (plan §5): fully certified = replayed witness + (exhaustive brute12force | externally checked DRAT certificate + proved lemma); solver-supported =13two agreeing solver paths without external certificate; candidate = upper only.14"""15import csv16import json17import math18import os1920import common2122R = common.RESULTS23HOLDOUT = {32, 35, 37, 41, 44, 48}24KNOWN = {11: ("6", "Rashidi et al. 2020 Thm 2.6; Krishnan 2026 exhaustive"),25 14: ("8", "P(14,5) ~ P(14,3); Krishnan-Ma-Zhang 2026 Thm 1.1"),26 16: ("8", "P(16,5) ~ P(16,3); Krishnan-Ma-Zhang 2026 Thm 1.1"),27 19: ("10", "P(19,5) ~ P(19,4); Krishnan-Ma-Zhang 2026 Thm 1.1"),28 21: ("10", "P(21,5) ~ P(21,4); Krishnan-Ma-Zhang 2026 Thm 1.1")}29RASHIDI_UB = {11: 6, 12: 8, 13: 10, 14: 11, 16: 9}303132def load_jsonl(name):33 p = os.path.join(R, name)34 return [json.loads(l) for l in open(p)] if os.path.exists(p) else []353637def main(nmax=48):38 bf = json.load(open(os.path.join(R, "brute_force_values.json"))) if os.path.exists(os.path.join(R, "brute_force_values.json")) else {}39 wit = {}40 for w in load_jsonl("upper_bound_witnesses.jsonl"):41 if w["n"] not in wit or w["size"] < wit[w["n"]]["size"]:42 wit[w["n"]] = w43 ubv = json.load(open(os.path.join(R, "upper_bound_verification.json"))) if os.path.exists(os.path.join(R, "upper_bound_verification.json")) else {"witnesses": [], "P7": []}44 replay_ok = {(x["n"], x["size"]): x["replay_ok"] for x in ubv["witnesses"]}45 p7_ok = {x["n"]: x["replay_ok"] for x in ubv["P7"]}46 lbv = json.load(open(os.path.join(R, "lower_bound_verification.json"))) if os.path.exists(os.path.join(R, "lower_bound_verification.json")) else {"boundary": [], "fortcover": []}47 bnd_ok = {(x["n"], x["p"]): x["ok"] for x in lbv["boundary"]}48 fort_ok = {(x["n"], x["bound"]): x["ok"] for x in lbv["fortcover"]}49 fort_certs = {}50 for c in load_jsonl("lower_bound_certificates.jsonl"):51 if c.get("sat") is False:52 fort_certs[c["n"]] = max(fort_certs.get(c["n"], -1), c["bound"])53 bnd_certs = {}54 for c in load_jsonl("boundary_certificates.jsonl"):55 if c.get("sat") is False and c["n"] >= math.ceil((c["p"] + 11) / 2):56 bnd_certs.setdefault(c["n"], []).append(c["p"])57 round_unsat = {}58 for r in load_jsonl("solver_runs.jsonl"):59 if r.get("method") == "round_sat" and r.get("sat") is False:60 round_unsat[r["n"]] = max(round_unsat.get(r["n"], -1), r["bound"])61 rows = []62 for n in range(11, nmax + 1):63 up = None64 up_src = []65 if n in wit:66 up = wit[n]["size"]67 up_src.append("witness(%d)%s" % (up, "" if replay_ok.get((n, up)) else "?"))68 if n >= 12 and p7_ok.get(n, n == 12 and p7_ok.get(12)):69 if up is None or 12 < up:70 up = 1271 up_src.append("P7")72 if str(n) in bf and bf[str(n)]["Z"] is not None:73 if up is None or bf[str(n)]["Z"] < up:74 up = bf[str(n)]["Z"]75 up_src.append("bruteforce-witness")76 low = 177 low_src = []78 if str(n) in bf and bf[str(n)]["Z"] is not None:79 low = max(low, bf[str(n)]["Z"])80 low_src.append("exhaustive(sizes<=%d)" % (bf[str(n)]["Z"] - 1))81 if n in bnd_certs:82 ps = [p for p in bnd_certs[n] if bnd_ok.get((n, p))]83 if ps:84 low = max(low, 12)85 low_src.append("boundary-DRAT(p=%s)+Lemma3.1" % ",".join(str(p) for p in sorted(ps)))86 if n in fort_certs and fort_ok.get((n, fort_certs[n])):87 low = max(low, fort_certs[n] + 1)88 low_src.append("fortcover-DRAT(b=%d)" % fort_certs[n])89 if n in round_unsat:90 low_ss = round_unsat[n] + 191 low_src.append("round-SAT-unsat(s=%d)[solver-supported]" % round_unsat[n])92 else:93 low_ss = 194 if up is not None and low == up and low_src:95 status = "fully certified"96 Z = up97 elif up is not None and max(low, low_ss) == up:98 status = "solver-supported"99 Z = up100 elif up is not None:101 status = "candidate"102 Z = ""103 else:104 status = "unknown"105 Z = ""106 rows.append({"n": n, "Z": Z, "upper": up if up is not None else "", "upper_evidence": ";".join(up_src),107 "lower": low if low_src else (low_ss if low_ss > 1 else ""), "lower_evidence": ";".join(low_src),108 "status": status, "holdout": n in HOLDOUT, "gcd_n_5": math.gcd(n, 5), "n_mod_24": n % 24})109 with open(os.path.join(R, "exact_values.csv"), "w", newline="") as f:110 w = csv.DictWriter(f, fieldnames=list(rows[0].keys()))111 w.writeheader()112 w.writerows(rows)113 # known vs new114 kv = []115 for r in rows:116 n = r["n"]117 if n in KNOWN:118 lit, src = KNOWN[n]119 elif n % 24 == 0:120 lit, src = "12", "Alameda et al. 2018 as reported by Rashidi et al. 2020 Remark 2.4 (second-hand)"121 else:122 lit, src = "", "no published exact value found (to our knowledge)"123 ub = RASHIDI_UB.get(n, 12)124 kv.append({"n": n, "published_value": lit, "published_source": src, "published_upper_bound": ub,125 "this_run_Z": r["Z"], "status": r["status"],126 "classification": ("known" if lit else ("new" if r["status"] == "fully certified" else ("new (solver-supported)" if r["status"] == "solver-supported" else "unresolved"))),127 "agrees_with_literature": ("" if not lit or r["Z"] == "" else str(int(lit) == r["Z"]))})128 with open(os.path.join(R, "known_vs_new.csv"), "w", newline="") as f:129 w = csv.DictWriter(f, fieldnames=list(kv[0].keys()))130 w.writeheader()131 w.writerows(kv)132 return rows, kv133134135if __name__ == "__main__":136 rows, kv = main()137 for r in rows:138 print(r["n"], r["Z"], r["status"], r["upper_evidence"], "|", r["lower_evidence"])139