1"""Numerical / symbolic checks accompanying the handwritten proofs in2results/derivations.md.34CS6 boundary identity: direct |dX| equals the layer formula5 |((U-1) u (U+1) u V) \\ U| + |((V-5) u (V+5) u U) \\ V| (k = 5), random X.6T8 deletion map of Lemma P9 (k = 5): for random X with >= 11 consecutive empty7 columns, deleting the middle column of the run preserves |X| and |dX|.8P6 the modular identity behind the isomorphism psi (sympy, symbolic in j).9L2 the counting inequalities of the finite reduction (sympy, exact integer10 arithmetic over the relevant ranges).11P7 index bookkeeping of the 12-vertex construction (sympy inequalities).12Output: results/lemma_checks.json and a line in results/experiment-log.jsonl.13"""14import json15import os16import random1718import common19import sympy as sp20from graph_constructor import adjacency, edges_formula, u, v2122K = 5232425def boundary_direct(n, k, X):26 adj = adjacency(n, k)27 Xs = set(X)28 return {w for x in X for w in adj[x] if w not in Xs}293031def boundary_formula(n, k, X):32 U = {x for x in X if x < n}33 V = {x - n for x in X if x >= n}34 outer = ({(i - 1) % n for i in U} | {(i + 1) % n for i in U} | V) - U35 inner = ({(i - k) % n for i in V} | {(i + k) % n for i in V} | U) - V36 return len(outer) + len(inner)373839def cs6(trials=300, seed=6):40 rng = random.Random(seed)41 bad = 042 total = 043 for n in range(13, 31):44 for _ in range(trials):45 X = rng.sample(range(2 * n), rng.randint(1, 2 * n - 1))46 total += 147 if len(boundary_direct(n, K, X)) != boundary_formula(n, K, X):48 bad += 149 return {"total": total, "mismatches": bad}505152def delete_column(n, k, X, col):53 """Deletes column col (both vertices must be outside X), reindexes columns > col down by one."""54 assert all((x % n) != col for x in X)5556 def f(i):57 return i if i < col else i - 15859 X2 = []60 for x in X:61 layer, i = (0, x) if x < n else (1, x - n)62 X2.append(f(i) if layer == 0 else (n - 1) + f(i))63 return X2646566def t8(trials=200, seed=8):67 rng = random.Random(seed)68 bad = 069 total = 070 for n in range(2 * K + 3, 41):71 for _ in range(trials):72 # choose a run of 11 consecutive empty columns starting at a random column a73 a = rng.randrange(n)74 empty = {(a + t) % n for t in range(2 * K + 1)}75 allowed = [w for w in range(2 * n) if (w % n) not in empty]76 if not allowed:77 continue78 X = rng.sample(allowed, rng.randint(1, len(allowed)))79 # rotate so that the empty run is columns 0..2k, then delete column k (P9 statement)80 shift = (-a) % n81 Xr = [((x + shift) % n) if x < n else n + ((x - n + shift) % n) for x in X]82 assert all((x % n) in range(2 * K + 1) or True for x in Xr)83 X2 = delete_column(n, K, Xr, K)84 total += 185 if len(X2) != len(Xr) or len(boundary_direct(n - 1, K, X2)) != len(boundary_direct(n, K, Xr)):86 bad += 187 return {"total": total, "mismatches": bad}888990def p6_symbolic():91 """For k*l = 1 (mod n): (j+l)*k = j*k + 1 (mod n) symbolically in j: (j+l)k - (jk+1) = lk - 1 = 0 mod n."""92 j, k, l, n, m = sp.symbols("j k l n m", integer=True)93 expr = sp.expand((j + l) * k - (j * k + 1))94 ok_symbolic = sp.simplify(expr - (l * k - 1)) == 095 # numeric instances for k = 5, 11 <= n <= 60, gcd(n,5) = 196 inst = []97 for nn in range(11, 61):98 if sp.gcd(nn, 5) != 1:99 continue100 ll = pow(5, -1, nn)101 inst.append(all(((jj + ll) * 5 - (jj * 5 + 1)) % nn == 0 for jj in range(nn)))102 return {"symbolic_identity": bool(ok_symbolic), "numeric_instances": len(inst), "numeric_all_ok": all(inst)}103104105def l2_symbolic():106 """2c - p <= 11 => c <= floor((p+11)/2); gaps <= 10 => n <= 11 c; forces count 2n - s >= p iff n >= (p+s)/2."""107 c, p, n, s = sp.symbols("c p n s", integer=True)108 rows = []109 for pp in range(12, 31):110 cmax = sp.floor((pp + 11) / sp.Integer(2))111 # check: every integer c with 2c - pp <= 11 satisfies c <= cmax, and c = cmax satisfies it112 ok = all((2 * cc - pp <= 11) == (cc <= cmax) for cc in range(0, 60))113 nmax = 11 * cmax114 nmin_forces = sp.ceiling((pp + 11) / sp.Integer(2))115 ok2 = all((2 * nn - 11 >= pp) == (nn >= nmin_forces) for nn in range(0, 200))116 rows.append({"p": pp, "c_max": int(cmax), "N_max": int(nmax), "n_min_forces": int(nmin_forces), "ok": bool(ok and ok2)})117 return rows118119120def p7_symbolic():121 """For j >= 12: j - 10 >= 2 and j - 5 >= 7, so the other neighbours of u_{j-1}, v_{j-5} lie in columns < j."""122 j = sp.symbols("j", integer=True)123 return {"j-10>=2 for j>=12": bool(sp.simplify((j - 10) - 2).subs(j, 12) >= 0) and all((jj - 10) >= 2 for jj in range(12, 500)),124 "j-5>=7 for j>=12": all((jj - 5) >= 7 for jj in range(12, 500))}125126127if __name__ == "__main__":128 out = {"CS6_boundary_identity": cs6(), "T8_deletion_map": t8(), "P6_isomorphism_identity": p6_symbolic(),129 "L2_counting": l2_symbolic(), "P7_index_bookkeeping": p7_symbolic(), "sympy_version": sp.__version__, "utc": common.utcnow()}130 with open(os.path.join(common.RESULTS, "lemma_checks.json"), "w") as f:131 json.dump(out, f, indent=1)132 common.log_event("D", "lemma_checks", CS6=out["CS6_boundary_identity"], T8=out["T8_deletion_map"],133 P6=out["P6_isomorphism_identity"], L2_all_ok=all(r["ok"] for r in out["L2_counting"]), P7=out["P7_index_bookkeeping"])134 print(json.dumps({k: v for k, v in out.items() if k != "L2_counting"}, indent=1))135 print("L2 rows ok:", all(r["ok"] for r in out["L2_counting"]), [(r["p"], r["c_max"], r["N_max"], r["n_min_forces"]) for r in out["L2_counting"] if r["p"] in (16, 18, 20, 22, 24)])136