1"""Stage 6: generate the LaTeX table fragments included by manuscript/main.tex.23Every number is read from results/ (exact_values.csv, known_vs_new.csv,4tables/*.csv, metrics.json, robustness/summary.json, lower_bound_certificates.jsonl,5solver_runs.jsonl). Output: results/tables/*.tex. Nothing is typed by hand.6"""7import csv8import json9import os1011ROOT = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))12os.chdir(ROOT)13T = "results/tables"141516def rd(path):17 return list(csv.DictReader(open(path)))181920def jl(path):21 return [json.loads(l) for l in open(path) if l.strip()]222324def num(x):25 """thousands separators"""26 return f"{int(x):,}"272829exact = rd("results/exact_values.csv")30kvn = {r["n"]: r for r in rd("results/known_vs_new.csv")}31metrics = json.load(open("results/metrics.json"))32summary = json.load(open("results/robustness/summary.json"))33bf = rd(f"{T}/brute_force.csv")34window = rd(f"{T}/boundary_window_p18.csv")35btab = rd(f"{T}/boundary_table.csv")36lbc = jl("results/lower_bound_certificates.jsonl")37ff_rows = {(r["n"], r["s"]): r for r in summary["ff_brute"]["rows"]}38fort_cert_n = set(r["n"] for r in lbc)3940# ---------------------------------------------------------------- Table: exact values41def lower_code(ev):42 codes = []43 if "exhaustive" in ev:44 codes.append("E")45 if "fortcover-DRAT" in ev:46 codes.append("F")47 if "boundary-DRAT" in ev:48 codes.append("B")49 if "round-SAT-unsat" in ev:50 codes.append("R")51 return codes525354def lit_cell(n):55 r = kvn[str(n)]56 if r["classification"] == "known":57 src = r["published_source"]58 if "Rashidi" in src and "Krishnan 2026" in src:59 return "6 (R20, K26)"60 if "P(14,5)" in src or "P(16,5)" in src:61 return f"{r['published_value']} (KMZ, $\\cong P({n},3)$)"62 if "P(19,5)" in src or "P(21,5)" in src:63 return f"{r['published_value']} (KMZ, $\\cong P({n},4)$)"64 if "Alameda" in src:65 return f"{r['published_value']} (A18$^\\dagger$)"66 return r["published_value"]67 return "---"686970rows = []71for r in exact:72 n = int(r["n"])73 ff = ff_rows.get((n, int(r["Z"]) - 1))74 codes = lower_code(r["lower_evidence"])75 if n in fort_cert_n and "F" not in codes:76 codes.insert(1, "F") # certificates for n = 21, 22 finished after exact_values.csv was written77 lc = "\\,".join(codes)78 if ff is not None and ff["forcing"] == 0:79 lc += "\\,E$'$"80 hold = "\\,$^{h}$" if r["holdout"] == "True" else ""81 newflag = "new" if kvn[str(n)]["classification"] == "new" else "known"82 rows.append((f"{n}{hold}", r["Z"], f"$\\le {kvn[str(n)]['published_upper_bound']}$", lit_cell(n), lc, newflag))8384half = (len(rows) + 1) // 285with open(f"{T}/tab_exact_values.tex", "w") as f:86 f.write("\\setlength{\\tabcolsep}{3pt}\\begin{tabular}{@{}rclllc@{\\hspace{8pt}}rclllc@{}}\n\\toprule\n")87 f.write("$n$ & $Z$ & bound & literature & lower & class & $n$ & $Z$ & bound & literature & lower & class\\\\\n\\midrule\n")88 for i in range(half):89 a = rows[i]90 b = rows[i + half] if i + half < len(rows) else ("", "", "", "", "", "")91 f.write(" & ".join(a) + " & " + " & ".join(b) + "\\\\\n")92 f.write("\\bottomrule\n\\end{tabular}\n")9394# ---------------------------------------------------------------- Table: exhaustive enumeration95bf_by = {}96for r in bf:97 bf_by.setdefault(int(r["n"]), {})[int(r["s"])] = r98Z = {int(r["n"]): int(r["Z"]) for r in exact}99with open(f"{T}/tab_brute_force.tex", "w") as f:100 f.write("\\setlength{\\tabcolsep}{4pt}\\begin{tabular}{@{}rrrrrrr@{}}\n\\toprule\n")101 f.write("$n$ & $Z$ & subsets, $s=Z-1$ & orbit reps.\\ tested & wall (s) & E$'$ sets, $s=Z-1$ & forcing reps., $s=Z$\\\\\n\\midrule\n")102 for n in range(11, 28):103 z = Z[n]104 lo = bf_by[n][z - 1]105 hi = bf_by[n].get(z)106 ff = ff_rows.get((n, z - 1))107 ffcell = num(ff["enumerated"]) if ff else "---"108 hicell = num(hi["forcing_representatives"]) if hi else "(P7 witness)"109 f.write(f"{n} & {z} & {num(lo['subsets'])} & {num(lo['orbit_representatives'])} & {float(lo['wall_seconds']):.1f} & {ffcell} & {hicell}\\\\\n")110 f.write("\\bottomrule\n\\end{tabular}\n")111112# ---------------------------------------------------------------- Table: beta_p(n) for n = 20..30113cols = [str(n) for n in range(20, 31)]114with open(f"{T}/tab_boundary_table.tex", "w") as f:115 f.write("\\begin{tabular}{@{}r" + "c" * len(cols) + "@{}}\n\\toprule\n")116 f.write("$p\\backslash n$ & " + " & ".join(cols) + "\\\\\n\\midrule\n")117 for r in btab:118 cells = []119 for c in cols:120 v = r[c]121 cells.append("$\\mathbf{\\ge 12}$" if v.startswith(">=") else v)122 f.write(f"{r['p']} & " + " & ".join(cells) + "\\\\\n")123 f.write("\\bottomrule\n\\end{tabular}\n")124125# ---------------------------------------------------------------- Table: certified window scaling126pick = [26, 30, 40, 50, 60, 70, 80, 90, 100, 110, 120, 130, 140, 150, 154]127wmap = {int(r["n"]): r for r in window}128with open(f"{T}/tab_window_scaling.tex", "w") as f:129 f.write("\\setlength{\\tabcolsep}{3.5pt}\\begin{tabular}{@{}rrrrrrll@{}}\n\\toprule\n")130 f.write("$n$ & variables & clauses & CaDiCaL (s) & proof lines & drat-trim (s) & CNF SHA-256 & proof SHA-256\\\\\n\\midrule\n")131 for n in pick:132 r = wmap[n]133 f.write(f"{n} & {num(r['num_vars'])} & {num(r['num_clauses'])} & {float(r['solve_seconds']):.1f} & {num(r['proof_lines'])} & {float(r['check_seconds']):.1f} & \\texttt{{{r['cnf_sha256']}}} & \\texttt{{{r['proof_sha256']}}}\\\\\n")134 f.write("\\bottomrule\n\\end{tabular}\n")135 f.write("%% totals: solve %s s, check %s s, proof lines %s\n" % (136 sum(float(r["solve_seconds"]) for r in window if int(r["n"]) >= 26),137 sum(float(r["check_seconds"]) for r in window if int(r["n"]) >= 26),138 sum(int(r["proof_lines"]) for r in window if int(r["n"]) >= 26)))139140# ---------------------------------------------------------------- Table: fort-cover certificates141seen = set()142with open(f"{T}/tab_fortcover.tex", "w") as f:143 f.write("\\begin{tabular}{@{}rrrrrrr@{}}\n\\toprule\n")144 f.write("$n$ & bound $b=Z-1$ & forts in $\\mathcal L$ & variables & clauses & proof lines & CaDiCaL (s)\\\\\n\\midrule\n")145 for r in sorted(lbc, key=lambda r: (r["n"], r["bound"])):146 if (r["n"], r["bound"]) in seen:147 continue148 seen.add((r["n"], r["bound"]))149 solve = f"{float(r['solve_seconds']):.2f}" if r.get("solve_seconds") is not None else "n/r$^{*}$"150 f.write(f"{r['n']} & {r['bound']} & {num(r['num_forts'])} & {num(r['num_vars'])} & {num(r['num_clauses'])} & {num(r['proof_lines'])} & {solve}\\\\\n")151 f.write("\\bottomrule\n\\end{tabular}\n")152153# ---------------------------------------------------------------- Table: independent paths per n154runs = jl("results/solver_runs.jsonl")155round_unsat = set(metrics["round_sat_unsat_agreements"])156round_to = set(metrics["round_sat_timeouts"])157fort_n = set(r["n"] for r in lbc)158boundary_n = set(range(26, 155)) | {24}159ffn = set(summary["ff_brute"]["size11_zero_forcing_n"]) | set(range(11, 23))160with open(f"{T}/tab_paths.tex", "w") as f:161 f.write("\\begin{tabular}{@{}rcccccc@{}}\n\\toprule\n")162 f.write("$n$ & $Z$ & exhaustive (E) & first-force (E$'$) & fort cover + DRAT (F) & round SAT (R) & boundary DRAT (B)\\\\\n\\midrule\n")163 for n in range(11, 41):164 z = Z.get(n, 12)165 e = "$\\bullet$" if n <= 27 else "--"166 ep = "$\\bullet$" if n in ffn else "--"167 fc_solver_only = {r["n"] for r in runs if r["method"] == "fort_cover" and r.get("sat") is False and r["n"] not in fort_n}168 fc = "$\\bullet$" if n in fort_n else ("(s)" if n in fc_solver_only else ("t/o" if n in metrics["holdout"] else "--"))169 round_to_only = {r["n"] for r in runs if r["method"] == "round_sat" and r.get("timeout")} - round_unsat170 rs = "$\\bullet$" if n in round_unsat else ("t/o" if n in round_to_only else "--")171 b = "$\\bullet$" if n in boundary_n else ("$\\times$" if n == 25 else "--")172 f.write(f"{n} & {z} & {e} & {ep} & {fc} & {rs} & {b}\\\\\n")173 f.write("\\bottomrule\n\\end{tabular}\n")174175# ---------------------------------------------------------------- Table: conjecture registry176conj = jl("plan/conjectures.jsonl")177final = {}178for c in conj:179 final.setdefault(c["id"], {}).update(c)180with open(f"{T}/tab_conjectures.tex", "w") as f:181 f.write("\\setlength{\\tabcolsep}{4pt}\\begin{tabular}{@{}lL{7.2cm}llL{2.2cm}@{}}\n\\toprule\n")182 f.write("id & statement (abridged) & registered & status & holdout (6 values)\\\\\n\\midrule\n")183 # abridged LaTeX renderings of the registered statements (plan/conjectures.jsonl is the source of record)184 abridged = {185 "H0": "Null hypothesis: every exact value of $Z(P(n,5))$ is already published.",186 "H4": "Small-$n$ exceptions: $P(11,5)$ and a few further small $n$ deviate from the eventual value.",187 "C1": "$Z(P(n,5))=12$ for every $n\\ge 26$.",188 "C2": "Threshold $n_0=23$; $Z(P(22,5))=11$; $Z=6,8,9,8,8,8,10,10,10,10,10,11$ for $n=11,\\dots,22$.",189 "C3": "Eventual periodicity (H2): $Z(P(n,5))$ is eventually constant (period $1$), not dependent on $n \\bmod m$ for $m\\in\\{2,3,4,5,6,8,10,12,24\\}$.",190 "C4": "Tightness (H3): for every $n\\ge 26$ the first-force bound with $p=18$ equals $Z$ (both $12$); for $n=25$ every $p\\le 24$ fails.",191 "C5": "$\\beta_{16}(n)\\le 11$ for every $n\\ge 22$: the $k=4$ parameter $p=16$ never certifies $Z(P(n,5))\\ge 12$.",192 }193 for cid in ["H0", "H4", "C1", "C2", "C3", "C4", "C5"]:194 c = final[cid]195 st = abridged[cid]196 hr = c.get("holdout_results")197 if hr:198 allpass = all(v["status"] == "pass" for v in hr.values())199 hcell = "6/6 pass" if allpass else "fail"200 else:201 hcell = "n/a"202 f.write(f"{cid} & {st} & {c['registered_utc'][11:19]} & {c['proof_status'].replace('_', ' ')} & {hcell}\\\\\n")203 f.write("\\bottomrule\n\\end{tabular}\n")204205# ---------------------------------------------------------------- Table: verification summary (robustness)206s = summary207with open(f"{T}/tab_verification.tex", "w") as f:208 f.write("\\begin{tabular}{@{}L{7.2cm}rr@{}}\n\\toprule\n")209 f.write("check (independent implementation) & instances & failures\\\\\n\\midrule\n")210 f.write(f"boundary certificates: CNF rebuilt, hashes, drat-trim rerun & {s['certificate_recheck']['boundary_checked']} & {s['certificate_recheck']['boundary_checked']-s['certificate_recheck']['boundary_ok']}\\\\\n")211 f.write(f"fort-cover certificates: forts revalidated, CNF rebuilt, drat-trim rerun & {s['certificate_recheck']['fortcover_checked']} & {s['certificate_recheck']['fortcover_checked']-s['certificate_recheck']['fortcover_ok']}\\\\\n")212 f.write(f"stored witnesses replayed force by force & {s['witness_replay']['witnesses']} & 0\\\\\n")213 f.write(f"P7 chronology replayed, $12\\le n\\le {s['witness_replay']['P7_range'][1]}$ & {s['witness_replay']['P7_range'][1]-11} & 0\\\\\n")214 f.write(f"enumeration counts vs.\\ binomial / Burnside orbit counts & {s['enumeration_counts']['rows']} & {s['enumeration_counts']['mismatches']}\\\\\n")215 f.write(f"boundary CNF vs.\\ exhaustive $\\beta_p(n)$ (UNSAT at $\\beta-1$, SAT at $\\beta$) & {s['boundary_encoding']['instances']} & {s['boundary_encoding']['instances'] - (s['boundary_encoding']['instances'] if s['boundary_encoding']['all_ok'] else 0)}\\\\\n")216 f.write(f"column-deletion map, exhaustive small sets (D1) & {s['deletion_lemma']['D1_cases']} & {s['deletion_lemma']['D1_failures']}\\\\\n")217 f.write(f"column-deletion negative control, 10 empty columns only (D2) & {s['deletion_lemma']['D2_cases']} & {s['deletion_lemma']['D2_boundary_size_changed']} (expected)\\\\\n")218 f.write(f"drat-trim negative controls (truncated / wrong CNF / satisfiable weakening) & 3 & 0\\\\\n")219 f.write(f"order independence of the closure (random orders) & {metrics['T2_total']} & {metrics['T2_total']-metrics['T2_passed']}\\\\\n")220 f.write(f"graph invariants, two constructors, $11\\le n\\le 48$ and $P(5,2)$ & {metrics['T1_n_count']} & 0\\\\\n")221 f.write("\\bottomrule\n\\end{tabular}\n")222223# ---------------------------------------------------------------- Table: formal / certificate scope224with open(f"{T}/tab_scope.tex", "w") as f:225 f.write("\\begin{tabular}{@{}L{4.6cm}L{4.2cm}L{4.6cm}c@{}}\n\\toprule\n")226 f.write("statement & human proof & machine-checked input & Lean 4\\\\\n\\midrule\n")227 f.write("P1--P5 (closure, forts, symmetry, SAT encoding, graph facts) & complete, all $n$ & empirical companions only & no\\\\\n")228 f.write("P6--P9 (isomorphism, 12-vertex bound, first-force lemma, column deletion) & complete, all $n$ & symbolic identity (sympy); replays $12\\le n\\le 300$ & no\\\\\n")229 f.write("Lemmas 3.1--3.5 (boundary machinery, CNF correctness) & complete, all $n$, $p$ & integer bookkeeping $12\\le p\\le 30$ & no\\\\\n")230 f.write(f"$Z\\ge 12$ for $26\\le n\\le 154$ & via Lemma 3.4 & {metrics['boundary_window_instances']} DRAT proofs, drat-trim exit 0 & no\\\\\n")231 f.write("$Z\\ge 12$ for $n>154$ & Lemmas 3.2--3.3 (no computation) & --- & no\\\\\n")232 f.write("$Z(P(n,5))$, $11\\le n\\le 27$ & P3 (orbit reduction) & exhaustive enumeration, two independent programs & no\\\\\n")233 f.write("$Z(P(n,5))\\ge$ table, $11\\le n\\le 22$ & Lemma 3.5, P2 & 12 fort-cover DRAT proofs & no\\\\\n")234 f.write("upper bounds, all $n$ & P7 & replayed chronologies & no\\\\\n")235 f.write("\\bottomrule\n\\end{tabular}\n")236237# ---------------------------------------------------------------- Table: minimum witnesses 11..22238bfv = json.load(open("results/brute_force_values.json"))239def tex_set(w):240 return "$\\{" + ",".join(f"{a[0]}_{{{a[1:]}}}" for a in w.split(",")) + "\\}$"241with open(f"{T}/tab_witnesses.tex", "w") as f:242 f.write("\\begin{tabular}{@{}rrlr@{}}\n\\toprule\n")243 f.write("$n$ & $Z$ & a minimum zero-forcing set (first orbit representative found) & forcing reps.\\ at size $Z$\\\\\n\\midrule\n")244 for n in range(11, 23):245 r = bfv[str(n)]246 hi = bf_by[n].get(int(r["Z"]))247 f.write(f"{n} & {r['Z']} & {tex_set(r['witness'])} & {num(hi['forcing_representatives']) if hi else '---'}\\\\\n")248 f.write("\\bottomrule\n\\end{tabular}\n")249250print("tables written:", sorted(x for x in os.listdir(T) if x.endswith(".tex")))251