1"""Stage 5: exhaustiveness audit of the C oracle (code/brute_force.c) from2its recorded counts alone.34For every row (n, s) of results/tables/brute_force.csv:5 * 'subsets' must equal C(2n, s): the Gosper enumeration (and the m06 splitting, where used) covered every s-subset;7 * 'orbit_representatives' must equal the number of D_n-orbits on8 s-subsets of V(P(n,5)), computed here by Burnside's lemma from the cycle9 structure of the 2n dihedral permutations (rotations: 2*gcd(n,a) cycles10 of length n/gcd(n,a); reflections i -> a-i: fixed vertices where 2i = a11 mod n, the rest in 2-cycles). Equality means the canonical-form filter12 tested exactly one subset per orbit, so by P3 nothing was skipped.13Also records, per n, that the exhausted sizes form the full range 1..Z-114(size monotonicity: a forcing set of size < Z-1 would extend to one of size15Z-1, so exhausting Z-1 alone already suffices; both are recorded).16Output: results/robustness/enumeration_counts_check.json17"""18import csv19import json20import math21import os2223ROOT = os.path.dirname(os.path.dirname(os.path.dirname(os.path.abspath(__file__))))24os.chdir(ROOT)252627def orbit_count(n, s):28 N = 2 * n29 tot = 030 for a in range(n): # rotations31 if a == 0:32 tot += math.comb(N, s)33 continue34 L = n // math.gcd(n, a)35 c = N // L36 tot += math.comb(c, s // L) if s % L == 0 else 037 for a in range(n): # reflections i -> a - i on both layers38 fp = 2 * sum(1 for i in range(n) if (2 * i - a) % n == 0)39 two = (N - fp) // 240 tot += sum(math.comb(fp, j) * math.comb(two, (s - j) // 2) for j in range(0, min(fp, s) + 1) if (s - j) % 2 == 0)41 assert tot % (2 * n) == 042 return tot // (2 * n)434445def main():46 rows = list(csv.DictReader(open("results/tables/brute_force.csv")))47 Z = {int(r["n"]): int(r["Z"]) for r in csv.DictReader(open("results/exact_values.csv"))}48 out = {"rows": [], "mismatches": 0}49 per_n = {}50 for r in rows:51 n, s = int(r["n"]), int(r["s"])52 sub, rep, forcing = int(r["subsets"]), int(r["orbit_representatives"]), int(r["forcing_representatives"])53 exp_sub, exp_rep = math.comb(2 * n, s), orbit_count(n, s)54 ok = sub == exp_sub and rep == exp_rep55 out["rows"].append({"n": n, "s": s, "subsets": sub, "binomial": exp_sub, "representatives": rep, "burnside_orbits": exp_rep, "forcing": forcing, "ok": ok})56 out["mismatches"] += (not ok)57 per_n.setdefault(n, {})[s] = forcing58 out["per_n"] = []59 for n in sorted(per_n):60 sizes = per_n[n]61 z = Z.get(n)62 exhausted = sorted(s for s, f in sizes.items() if f == 0)63 found = sorted(s for s, f in sizes.items() if f > 0)64 out["per_n"].append({"n": n, "Z_table": z, "sizes_with_no_forcing_set": exhausted, "sizes_with_forcing_set": found,65 "size_Z_minus_1_exhausted": (z - 1) in exhausted if z else None,66 "all_sizes_1_to_Z_minus_1_exhausted": all(s in exhausted for s in range(1, z)) if z else None,67 "consistent_with_Z": (z is not None and (z - 1) in exhausted and all(s >= z for s in found))})68 out["all_rows_ok"] = out["mismatches"] == 069 out["all_n_consistent"] = all(p["consistent_with_Z"] for p in out["per_n"])70 json.dump(out, open("results/robustness/enumeration_counts_check.json", "w"), indent=1)71 print("rows", len(rows), "mismatches", out["mismatches"], "all n consistent with Z:", out["all_n_consistent"])72 for p in out["per_n"]:73 print(p["n"], p["Z_table"], "exhausted", p["sizes_with_no_forcing_set"], "found", p["sizes_with_forcing_set"], "all 1..Z-1:", p["all_sizes_1_to_Z_minus_1_exhausted"])747576if __name__ == "__main__":77 main()78