An explicit degree-3 counterexample to the Jacobian Conjecture

"""Standalone verification of the degree-3 Jacobian-conjecture counterexample.

Reads degree3_map.json (same directory), rebuilds the 19-variable map in sympy,
and checks:
  1. every component has total degree <= 3 (and the max is exactly 3);
  2. det J = -2 identically;
  3. the three listed rational points are distinct and share one image.

For (2) it uses the map's structure: the w-block of J is I + L with L
nilpotent (the carrier dependency graph is acyclic), so
    det J = det(I+L) * det( A - B (I+L)^{-1} C ) = det( A - B (I+L)^{-1} C )
with (I+L)^{-1} = sum_j (-L)^j.  Nilpotence is asserted by computing the
series to exact termination, and the inverse identity is asserted too --
nothing is assumed.  Everything is exact over Q.
A brute-force cross-check, sympy.Matrix(J).det(), gives the same answer if
you have the patience.

Requires: sympy >= 1.12.   Run:  python verify_degree3.py
"""
import json
import os

import sympy as sp

HERE = os.path.dirname(os.path.abspath(__file__))
d = json.load(open(os.path.join(HERE, "degree3_map.json"), encoding="utf-8"))
N = d["N"]
m = N - 3

names = ["x", "y", "z"] + [f"w{k}" for k in range(1, m + 1)]
syms = sp.symbols(names)
sd = dict(zip(names, syms))


def parse_mono(ms):
    if ms == "1":
        return sp.Integer(1)
    e = sp.Integer(1)
    for part in ms.split("*"):
        if "^" in part:
            v, p = part.split("^")
            e *= sd[v] ** int(p)
        else:
            e *= sd[part]
    return e


comps = [
    sp.expand(sum(sp.Rational(c) * parse_mono(mo) for mo, c in cd.items()))
    for cd in d["components"]
]

# --- 1. degree ------------------------------------------------------------
degs = [sp.total_degree(sp.Poly(c, *syms)) for c in comps]
assert max(degs) == 3, f"degree check failed: {degs}"
print(f"[1/3] component degrees {degs} -> max 3: OK")

# --- 2. det J -------------------------------------------------------------
J = sp.Matrix([[sp.diff(c, v) for v in syms] for c in comps])
A = J[:3, :3]
B = J[:3, 3:]
C = J[3:, :3]
D = J[3:, 3:]

L = D - sp.eye(m)
Winv = sp.zeros(m)
term = sp.eye(m)
for _ in range(m + 1):
    Winv += term
    term = sp.expand(term * (-L))
    if term.is_zero_matrix:
        break
assert term.is_zero_matrix, "w-block is not unipotent (L not nilpotent)!"
assert sp.expand(Winv * (sp.eye(m) + L)) == sp.eye(m)
S = sp.expand(A - B * Winv * C)
det = sp.expand(S.det(method="berkowitz"))
assert det == -2, f"det = {det}"
print("[2/3] det J = -2 identically: OK  (unipotent w-block asserted)")

# --- 3. collision ---------------------------------------------------------
pts = [{sd[k]: sp.Rational(v) for k, v in p.items()} for p in d["points"]]
imgs = [tuple(c.subs(p) for c in comps) for p in pts]
assert imgs[0] == imgs[1] == imgs[2], "images differ!"
assert pts[0] != pts[1] and pts[1] != pts[2] and pts[0] != pts[2], "points coincide!"
print(f"[3/3] three distinct points, one image: OK  (image begins {imgs[0][:4]})")

print("\nAll checks passed: degree-3 Keller map, det J = -2, not injective.")