"""Numerical / symbolic checks accompanying the handwritten proofs in
results/derivations.md.

CS6  boundary identity: direct |dX| equals the layer formula
     |((U-1) u (U+1) u V) \\ U| + |((V-5) u (V+5) u U) \\ V|  (k = 5), random X.
T8   deletion map of Lemma P9 (k = 5): for random X with >= 11 consecutive empty
     columns, deleting the middle column of the run preserves |X| and |dX|.
P6   the modular identity behind the isomorphism psi (sympy, symbolic in j).
L2   the counting inequalities of the finite reduction (sympy, exact integer
     arithmetic over the relevant ranges).
P7   index bookkeeping of the 12-vertex construction (sympy inequalities).
Output: results/lemma_checks.json and a line in results/experiment-log.jsonl.
"""
import json
import os
import random

import common
import sympy as sp
from graph_constructor import adjacency, edges_formula, u, v

K = 5


def boundary_direct(n, k, X):
    adj = adjacency(n, k)
    Xs = set(X)
    return {w for x in X for w in adj[x] if w not in Xs}


def boundary_formula(n, k, X):
    U = {x for x in X if x < n}
    V = {x - n for x in X if x >= n}
    outer = ({(i - 1) % n for i in U} | {(i + 1) % n for i in U} | V) - U
    inner = ({(i - k) % n for i in V} | {(i + k) % n for i in V} | U) - V
    return len(outer) + len(inner)


def cs6(trials=300, seed=6):
    rng = random.Random(seed)
    bad = 0
    total = 0
    for n in range(13, 31):
        for _ in range(trials):
            X = rng.sample(range(2 * n), rng.randint(1, 2 * n - 1))
            total += 1
            if len(boundary_direct(n, K, X)) != boundary_formula(n, K, X):
                bad += 1
    return {"total": total, "mismatches": bad}


def delete_column(n, k, X, col):
    """Deletes column col (both vertices must be outside X), reindexes columns > col down by one."""
    assert all((x % n) != col for x in X)

    def f(i):
        return i if i < col else i - 1

    X2 = []
    for x in X:
        layer, i = (0, x) if x < n else (1, x - n)
        X2.append(f(i) if layer == 0 else (n - 1) + f(i))
    return X2


def t8(trials=200, seed=8):
    rng = random.Random(seed)
    bad = 0
    total = 0
    for n in range(2 * K + 3, 41):
        for _ in range(trials):
            # choose a run of 11 consecutive empty columns starting at a random column a
            a = rng.randrange(n)
            empty = {(a + t) % n for t in range(2 * K + 1)}
            allowed = [w for w in range(2 * n) if (w % n) not in empty]
            if not allowed:
                continue
            X = rng.sample(allowed, rng.randint(1, len(allowed)))
            # rotate so that the empty run is columns 0..2k, then delete column k (P9 statement)
            shift = (-a) % n
            Xr = [((x + shift) % n) if x < n else n + ((x - n + shift) % n) for x in X]
            assert all((x % n) in range(2 * K + 1) or True for x in Xr)
            X2 = delete_column(n, K, Xr, K)
            total += 1
            if len(X2) != len(Xr) or len(boundary_direct(n - 1, K, X2)) != len(boundary_direct(n, K, Xr)):
                bad += 1
    return {"total": total, "mismatches": bad}


def p6_symbolic():
    """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."""
    j, k, l, n, m = sp.symbols("j k l n m", integer=True)
    expr = sp.expand((j + l) * k - (j * k + 1))
    ok_symbolic = sp.simplify(expr - (l * k - 1)) == 0
    # numeric instances for k = 5, 11 <= n <= 60, gcd(n,5) = 1
    inst = []
    for nn in range(11, 61):
        if sp.gcd(nn, 5) != 1:
            continue
        ll = pow(5, -1, nn)
        inst.append(all(((jj + ll) * 5 - (jj * 5 + 1)) % nn == 0 for jj in range(nn)))
    return {"symbolic_identity": bool(ok_symbolic), "numeric_instances": len(inst), "numeric_all_ok": all(inst)}


def l2_symbolic():
    """2c - p <= 11  =>  c <= floor((p+11)/2); gaps <= 10 => n <= 11 c; forces count 2n - s >= p iff n >= (p+s)/2."""
    c, p, n, s = sp.symbols("c p n s", integer=True)
    rows = []
    for pp in range(12, 31):
        cmax = sp.floor((pp + 11) / sp.Integer(2))
        # check: every integer c with 2c - pp <= 11 satisfies c <= cmax, and c = cmax satisfies it
        ok = all((2 * cc - pp <= 11) == (cc <= cmax) for cc in range(0, 60))
        nmax = 11 * cmax
        nmin_forces = sp.ceiling((pp + 11) / sp.Integer(2))
        ok2 = all((2 * nn - 11 >= pp) == (nn >= nmin_forces) for nn in range(0, 200))
        rows.append({"p": pp, "c_max": int(cmax), "N_max": int(nmax), "n_min_forces": int(nmin_forces), "ok": bool(ok and ok2)})
    return rows


def p7_symbolic():
    """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."""
    j = sp.symbols("j", integer=True)
    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)),
            "j-5>=7 for j>=12": all((jj - 5) >= 7 for jj in range(12, 500))}


if __name__ == "__main__":
    out = {"CS6_boundary_identity": cs6(), "T8_deletion_map": t8(), "P6_isomorphism_identity": p6_symbolic(),
           "L2_counting": l2_symbolic(), "P7_index_bookkeeping": p7_symbolic(), "sympy_version": sp.__version__, "utc": common.utcnow()}
    with open(os.path.join(common.RESULTS, "lemma_checks.json"), "w") as f:
        json.dump(out, f, indent=1)
    common.log_event("D", "lemma_checks", CS6=out["CS6_boundary_identity"], T8=out["T8_deletion_map"],
                     P6=out["P6_isomorphism_identity"], L2_all_ok=all(r["ok"] for r in out["L2_counting"]), P7=out["P7_index_bookkeeping"])
    print(json.dumps({k: v for k, v in out.items() if k != "L2_counting"}, indent=1))
    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)])