# -*- coding: utf-8 -*-
"""
DC_1 HUNTER — core engine + first exclusion sweep.

Target: the Dixmier conjecture for A_1 (open since 1968). A counterexample is
P, Q in A_1 = C<x, d> with [Q, P] = 1 such that x->P, d->Q is a non-surjective
endomorphism. Tsuchimoto / Belov-Kanel--Kontsevich: JC_{2n} => DC_n, so
NOT DC_1 => NOT JC_2 — killing the last open dimension of the Jacobian problem.

This file:
  1. exact Weyl algebra engine (normal-ordered x^a d^b, rational/symbolic coeffs)
  2. engine self-tests against known identities
  3. SWEEP 1: two-term sparse ansatz P = x + a*x^p d^q, Q = d + b*x^r d^s over
     all (p,q,r,s) with filtration weight <= 4; solve [Q,P]=1 exactly for (a,b);
     classify every solution family as tame/triangular or NOT.
Output: exclusion certificate for this ansatz class + any anomalies flagged.
"""
import sympy as sp
from sympy import Rational, binomial, ff
import itertools, time, json

t0 = time.time()

def wmul(A, B):
    """Product in A_1 with normal order x^a d^b. (a,b)*(c,e):
    d^b x^c = sum_k C(b,k) ff(c,k) x^(c-k) d^(b-k)."""
    out = {}
    for (a, b), ca in A.items():
        for (c, e), cb in B.items():
            for k in range(0, min(b, c) + 1):
                key = (a + c - k, b + e - k)
                out[key] = sp.expand(out.get(key, 0) + ca*cb*binomial(b, k)*ff(c, k))
    return {k: v for k, v in out.items() if v != 0}

def wsub(A, B):
    out = dict(A)
    for k, v in B.items():
        out[k] = sp.expand(out.get(k, 0) - v)
    return {k: v for k, v in out.items() if v != 0}

def comm(A, B):
    return wsub(wmul(A, B), wmul(B, A))

X = {(1, 0): sp.Integer(1)}
D = {(0, 1): sp.Integer(1)}
ONE = {(0, 0): sp.Integer(1)}

# --- engine self-tests ------------------------------------------------------
assert comm(D, X) == ONE, "[d,x] must be 1"
# triangular automorphism image: P = x, Q = d + x^2  -> [Q,P] = 1
Q_tri = {(0,1): sp.Integer(1), (2,0): sp.Integer(1)}
assert comm(Q_tri, X) == ONE
# symplectic swap: P = -d, Q = x -> [Q,P] = [x,-d] = 1
assert comm(X, {(0,1): sp.Integer(-1)}) == ONE
# a genuinely noncommuting pair: [d^2, x^2] = 4xd + 2
c = comm({(0,2): sp.Integer(1)}, {(2,0): sp.Integer(1)})
assert c == {(1,1): sp.Integer(4), (0,0): sp.Integer(2)}, c
print("[PASS] Weyl engine self-tests (normal ordering, commutators, known automorphisms)")

# --- SWEEP 1 ----------------------------------------------------------------
a, b = sp.symbols('a b')
MAXW = 4          # filtration weight cap p+q <= MAXW
results = []
anomalies = []
n_patterns = 0
for p, q in itertools.product(range(0, MAXW+1), repeat=2):
    if p + q < 2 or p + q > MAXW:      # need genuinely higher-order terms
        continue
    for r, s in itertools.product(range(0, MAXW+1), repeat=2):
        if r + s < 2 or r + s > MAXW:
            continue
        n_patterns += 1
        P = {(1,0): sp.Integer(1), (p,q): a}
        Q = {(0,1): sp.Integer(1), (r,s): b}
        E = wsub(comm(Q, P), ONE)      # must be 0
        eqs = [sp.expand(v) for v in E.values()]
        sols = sp.solve(eqs, [a, b], dict=True)
        for sol in sols:
            av = sol.get(a, a); bv = sol.get(b, b)
            if av == 0 or bv == 0:
                continue               # tame/triangular (one perturbation absent)
            # nontrivial two-sided solution -> classify
            results.append({"P_term": (p,q), "Q_term": (r,s), "a": str(av), "b": str(bv)})
            # triangular test: pure-x or pure-d perturbations commute with partner
            triangular = (q == 0 and s == 0) or (p == 0 and r == 0)
            if not triangular:
                anomalies.append({"P_term": (p,q), "Q_term": (r,s), "a": str(av), "b": str(bv)})

print(f"[DONE] SWEEP 1: {n_patterns} sparse two-term ansatz patterns, filtration weight <= {MAXW}")
print(f"        nontrivial (a,b both nonzero) solution families: {len(results)}")
print(f"        NON-TRIANGULAR anomalies (worth eyes): {len(anomalies)}")
for r in results:
    tag = "ANOMALY" if r in [dict(x_) for x_ in anomalies] else "triangular-class"
    print(f"        P=x+a*x^{r['P_term'][0]}d^{r['P_term'][1]}, "
          f"Q=d+b*x^{r['Q_term'][0]}d^{r['Q_term'][1]}  "
          f"a={r['a']} b={r['b']}  [{tag}]")

cert = {
    "sweep": "DC1 sparse two-term ansatz, filtration weight <= 4",
    "patterns_tested": n_patterns,
    "nontrivial_solution_families": results,
    "non_triangular_anomalies": anomalies,
    "engine": "exact normal-ordered Weyl algebra, sympy rational/symbolic",
    "conclusion": ("All commuting-pair solutions in this ansatz class are "
                   "triangular/tame images (or listed as anomalies above). "
                   "Exclusion data banked; next sweeps: 3-term ansatz, "
                   "equivariant seeds from Alpoge Mechanism II, weight 6-8."),
    "elapsed_sec": round(time.time()-t0, 2)
}
with open('post-jc-program/breakthrough/dc1_sweep1.json', 'w', encoding='utf-8') as fh:
    json.dump(cert, fh, indent=2)
print(f"\nartifact: dc1_sweep1.json  ({cert['elapsed_sec']}s)")