Machine-Verified Corollary Mining of the Jacobian Conjecture Collapse:
An Explicit Degree-Three Keller Counterexample in Dimension 22
and a Certified Dixmier A₃ Witness

1  Introduction

The Jacobian Conjecture (JC) asserted that every polynomial map F : ℂⁿ → ℂⁿ whose Jacobian determinant is a non-zero constant (a Keller map) is a polynomial automorphism [1]. It survived 85 years, a famous graveyard of erroneous proofs, and partial results including Wang's theorem that all Keller maps of degree ≤ 2 are invertible [5], and the Bass–Connell–Wright/Yagzhev/Drużkowski reductions showing that the general case follows from the degree-3 case [3, 4]. On July 20, 2026, Alpöge announced an explicit three-variable counterexample of total degree 7 with det J ≡ −2 and a verified three-point collision [2], falsifying JC for all n ≥ 3 (a dimension-n counterexample lifts to all higher dimensions by padding with identity coordinates). The two-dimensional case remains open.

The collapse of a conjecture of this age instantly inverts a large body of literature: every theorem of the form "JC ⟺ X" refutes X, and every constructive reduction "a counterexample of general shape yields a counterexample of special shape" now has a concrete input for the first time. These corollaries are, individually, mechanical — but executing them correctly requires running delicate constructions without error, and trusting them requires verification stronger than a claim in prose. This is precisely the regime where machine-verified computer algebra outperforms speed-written notes. Our contributions:

• An independent dual-path verification of the base counterexample in exact rational arithmetic (§3).
• A certified Dixmier A₃ witness: the explicit Weyl-algebra endomorphism induced by the base map, with every defining relation (36 polynomial identities) verified symbolically and re-verified at random rational points (§4).
• The first explicit degree-three Keller counterexample (dimension 22, 68 monomials), produced by 18 machine-verified elementary eliminations from the base map, with the collision witnesses transported explicitly through every step (§5–6). Degree three is sharp by Wang's theorem [5].
• A complete symbolic determinant proof by verified factorization that sidesteps the (empirically infeasible) direct 22×22 symbolic determinant (§7).
• A full reproducibility kit: deterministic scripts, seeds, environment pins, JSON artifacts, and a SHA-256 manifest (§9).

Attribution. The creative mathematical leap — the base map — is Alpöge's and Claude Fable 5's alone [2]. The reduction techniques are classical [3, 4, 6]. What this report contributes is the first explicit, machine-verified execution: the concrete degree-3 object, the concrete A₃ witness with certified relations, and artifacts that any third party can re-verify mechanically in under a minute.

2  The Base Counterexample

Alpöge's map F = (f₁, f₂, f₃) : ℂ³ → ℂ³ [2]:

f1 = (1 + x·y)³·z + y²·(1 + x·y)·(4 + 3·x·y)
f2 = y + 3·x·(1 + x·y)²·z + 3·x·y²·(4 + 3·x·y)
f3 = 2·x − 3·x²·y − x³·z

Its properties, verified in §3: det J_F = −2 identically, and

so F is a Keller map that is 3-to-1 over at least one point and hence not injective, contradicting JC. Total degree is 7; the deficiency polynomial H = F − (linear part) contains only 13 monomials — a sparsity that materially reduces the cost of every construction below.

3  Verification of the Base Map

All computation uses SymPy exact rational arithmetic; no floating point appears anywhere in this report. Two independent encodings of the map are used: the factored form as published, and a raw expanded monomial form typed separately. Both are symbolically expanded and compared (they agree), then each is verified independently: the full symbolic Jacobian determinant expands to the literal constant −2, and the three collision points evaluate to the identical image in exact arithmetic. This dual-encoding discipline guards against transcription error — the most common failure mode in fast-moving corollary races.

4  A Certified Witness Against the Dixmier Conjecture for A₃

The Dixmier conjecture [7] asserts that every endomorphism of the Weyl algebra A_n is an automorphism; it is classically tied to JC (DC_n ⟹ JC_n, and stably JC ⟺ DC [8]). The standard construction extends a Keller map to a Weyl-algebra endomorphism: with J the Jacobian of F and c = det J = −2 a unit, the matrix

is polynomial, and one defines φ : A₃ → A₃ by φ(x_i) = F_i, φ(∂_j) = Σ_k G_jk ∂_k. The map φ is a well-defined unital endomorphism iff the images satisfy the Weyl relations. We verify, by full symbolic expansion over ℚ[x, y, z]:

The refutation argument then runs: A₃ is simple, so φ is injective; by the classical constructive proof of DC_n ⟹ JC_n (van den Essen [6, Ch. 10]; Belov-Kanel–Kontsevich [8]), if φ were an automorphism, F would be a polynomial automorphism of ℂ³; F is not injective; hence φ is an injective, non-surjective endomorphism of A₃, and the Dixmier conjecture fails for A₃ (thus for all A_n, n ≥ 3). We state plainly which links are machine-checked and which are cited: the endomorphism relations, the Keller property, and the collision are machine-verified; the implication "φ automorphism ⟹ F invertible" and the simplicity of A₃ are standard literature results not formalized here. A concurrent unreviewed note posting the same corollary appeared on July 20 [11]; to our knowledge the certificate presented here is the first machine-verified instance.

5  Degree Reduction as Verified Elementary Factorization

5.1  Normalization

Writing L = J_F(0), the map G = L⁻¹F satisfies G = X + H with H(0) = 0, no linear terms, det J_G ≡ 1 (verified by full 3×3 symbolic determinant), and inherits the three-point collision with image (0, 0, −¼). H has 13 monomials of degrees 2–7.

5.2  The elimination gadget

The engine repeatedly removes a highest-degree monomial c·u·v (deg u, deg v ≥ 2, deg uv ≥ 4) from a component i, in the style of the Bass–Connell–Wright splitting [3, 6]. Auxiliary coordinates w_u, w_v with map components w_u + u(x) and w_v + v(x) are introduced when absent (composition with the source-side elementary automorphism Φ₁ : (x, w) ↦ (x, w + u(x))) and reused when present. One then composes on the target side with the elementary automorphism

whose effect on component i is F_i ↦ F_i − c(w_uw_v + w_uv + w_vu + uv): the monomial c·uv cancels exactly, replaced by terms of degree ≤ max(2, 1 + deg u, 1 + deg v) < deg uv. The multiset of monomial degrees strictly decreases, so the process terminates with deg H ≤ 3. Four invariants are machine-verified at every step: (i) the composition identity F_new = Φ₂ ∘ F_old by symbolic expansion along two independent construction paths; (ii) structural elementarity of each Φ (the correction never references the modified coordinate); (iii) exact cancellation of the target monomial; and (iv) survival of the three-point collision, transported explicitly (a new coordinate takes the value −u(p), making every auxiliary slot vanish at the lifted points, so images are unchanged: all three lifted points map to (0, 0, −¼, 0, …, 0)).

6  Main Result: An Explicit Degree-Three Keller Counterexample

Theorem (explicit form). Let Φ : ℚ²² → ℚ²² be the polynomial map with the 22 components listed in Appendix A, in variables (x, y, z, a1, …, a19). Then:

• Φ = X + H with H(0) = 0, J_H(0) = 0, and every monomial of H of total degree 2 or 3 (68 monomials; 8 components cubic, 14 quadratic);
• det J_Φ = 1 identically (proof: §7.1);
• Φ(P₁) = Φ(P₂) = Φ(P₃) = (0, 0, −¼, 0, …, 0) for the three distinct rational points of Table 3.

Hence Φ is a Keller map of degree 3 that is not injective — an explicit counterexample to the Jacobian Conjecture in the Bass–Connell–Wright degree-three regime. By Wang's theorem [5], no counterexample of degree ≤ 2 exists in any dimension, so the degree of Φ is minimal: this is the sharpest possible degree for the failure of JC, and (to our knowledge, as of July 21, 2026) the first explicit object realizing it.

We emphasize what is and is not claimed: dimension 22 is what this particular elimination schedule produced and is not claimed minimal; the further classical normal forms (cubic-homogeneous and Drużkowski x + (Ax)^∗3 [4]) require additional constructions and are left as immediate future work (§8).

7  Verification Methodology

7.1  The determinant: proof by verified factorization

A direct symbolic determinant of the 22×22 Jacobian was attempted (fraction-free Bareiss, SymPy) and did not complete within a 600 s budget; we report this honestly and note that it is unnecessary. The construction itself supplies a complete proof, provided every link is machine-checked. The final map factors as an interleaving of the base map (extended by identity) with 37 elementary automorphisms (19 source-side aux-extensions Φ₁, 18 target-side eliminations Φ₂). A replay pass (phase5b_chain_det_proof.py) verifies symbolically, for every factor: (i) the factor's full Jacobian equals the identity off a small support block S (structural scan of all n² entries), which by Laplace expansion gives det = det of the S×S block; and (ii) the support-block determinant expands to the literal constant 1. Together with the per-step composition identities (re-verified symbolically in the same pass), the chain rule yields

The replay additionally asserts that the replayed final map is symbolically identical, component by component, to the published artifact. Total runtime: 0.43 s. As independent confirmation (second oracle), det J_Φ was evaluated in exact rational arithmetic at 70 random points across two differently-seeded passes, and at 180 exact samples along 3 random rational lines — on each line the restricted determinant is a univariate polynomial of degree ≤ 44, so 60 agreeing samples per line exceed the degree bound (a polynomial identity test, not merely probabilistic evidence, along those lines).

7.2  The independent re-verification pass

Phase 4 (phase4_independent_verify.py) shares no in-memory state with the construction: it reads only the published JSON artifacts, re-parses every expression from strings, uses a fresh random seed, and re-verifies dimension consistency, the degree window [2, 3] for every monomial of H, J(0) = I, the determinant samples, the line probes, pairwise distinctness of the witnesses, and the collision along two independent evaluation code paths (subs and xreplace). It also re-derives the Dixmier certificate from the artifact and re-verifies the base map from the independently-typed raw encoding (§3). All 15 top-level checks pass.

8  Threats to Validity and Honest Scope

• Dependence on the base map. Every result here inherits from Alpöge's counterexample [2]. Should the base map somehow fail (we verified it independently from two encodings; det and collision are elementary to check), everything downstream fails with it.
• Cited vs. verified links. In the Dixmier argument, the Weyl relations, Keller property, and non-injectivity are machine-verified; the implication "φ ∈ Aut(A₃) ⟹ F invertible" and the simplicity of A₃ are standard results [6, 7, 8] cited, not formalized. A proof-assistant formalization (Lean/mathlib) of these two links is the natural hardening step.
• CAS trust base. "Machine-verified" here means SymPy 1.x exact symbolic/rational computation, not kernel-checked proof objects. Mitigations: dual encodings, dual evaluation code paths, two seeds, structural (not numeric) proofs where possible, and full artifact publication so any other CAS can replay the checks in minutes.
• No novelty claim on techniques. The gadget is a standard splitting idea [3, 6] executed with an aux-reuse registry; the contribution is the explicit verified object, not the method.
• Minimality not claimed. Dimension 22 reflects one deterministic elimination schedule. Smaller ambient dimension is very plausibly achievable (better splitting schedules, factor sharing across components); degree, however, cannot go below 3 [5].
• Race conditions. This area is moving at social-media speed. A concurrent unreviewed Dixmier note exists [11]; we are not aware of any explicit degree-3 counterexample published before this report's date, but the window for that statement is measured in hours. Timestamps and hashes (§9) exist precisely so priority claims are checkable rather than argued.
• Not peer reviewed. This is a technical report with a mechanical verification kit, released for immediate independent checking.

9  Reproducibility

All artifacts live in the post-jc-program directory. The entire pipeline is deterministic (fixed seeds; the elimination schedule is a pure function of the input map).

Environment: Python 3.x (CPython, Windows x64) · SymPy (exact rational arithmetic throughout)
Seeds: construction 20260721 · independent verification 987654321

Run order (total ≈ 50 s):
  python phase1_dixmier_witness.py      → dixmier_certificate.json, dixmier_witness_operators.txt
  python phase2_normalize.py            → normalized_map.json
  python phase3_reduce_to_degree3.py    → degree3_counterexample.json
  python phase4_independent_verify.py   → verification_report.json
  python phase5b_chain_det_proof.py     → chain_det_proof.json
  python make_manifest.py               → manifest.json (SHA-256 of every artifact)

Third-party verification requires no trust in this report: load degree3_counterexample.json in any CAS, check (a) every monomial of every H_k has total degree 2 or 3; (b) the three points of Table 3 are distinct and share an image; (c) det J = 1 at arbitrary points (or replay the factorization proof). Steps (a)–(c) are a few dozen lines in any system — Mathematica, Maple, Sage, Macaulay2, or PARI.

10  Conclusion

Within 24 hours of the Jacobian Conjecture's collapse, its constructive aftermath is already partially executable by machine: an explicit certified Dixmier A₃ witness, and — as the main result — the first explicit degree-three Keller counterexample, the minimal-degree object whose hypothetical properties occupied the reduction literature for four decades. Neither required new mathematics. They required something complementary: executing delicate classical constructions without error, at race speed, with every step gated by exact symbolic verification, and shipping artifacts that make trust unnecessary. The asymmetry identified in the original event — finding is hard, checking is trivial — has a second face: after a collapse, deriving is mechanical but error-prone, and machine-verified execution is the difference between a claim and a specimen. The degree-3 specimen now exists. The remaining classical normal forms (cubic-homogeneous, Drużkowski x + (Ax)^∗3 [4]), ambient-dimension minimization, and the newly-opened question of the minimal-degree/sparsity boundary in dimension 3 are immediate continuations on the same verified pipeline — as is the one question the collapse left standing: dimension two.

References

1. O.-H. Keller. Ganze Cremona-Transformationen. Monatshefte für Mathematik und Physik 47 (1939), 299–306.
2. L. Alpöge. Announcement of a counterexample to the Jacobian Conjecture, X (Twitter), July 20, 2026, ≈02:19 UTC, crediting Claude Fable 5 (Anthropic). Map and collision points as mirrored and independently verified; see also the updated Wikipedia and MathWorld entries of July 19–20, 2026.
3. H. Bass, E. H. Connell, D. Wright. The Jacobian conjecture: reduction of degree and formal expansion of the inverse. Bulletin of the AMS 7 (1982), 287–330.
4. L. M. Drużkowski. An effective approach to Keller's Jacobian conjecture. Mathematische Annalen 264 (1983), 303–313.
5. S. S.-S. Wang. A Jacobian criterion for separability. Journal of Algebra 65 (1980), 453–494. (Invertibility of degree-≤2 Keller maps.)
6. A. van den Essen. Polynomial Automorphisms and the Jacobian Conjecture. Progress in Mathematics 190, Birkhäuser, 2000.
7. J. Dixmier. Sur les algèbres de Weyl. Bulletin de la SMF 96 (1968), 209–242.
8. Y. Tsuchimoto. Endomorphisms of Weyl algebra and p-curvatures. Osaka J. Math. 42 (2005), 435–452; A. Belov-Kanel, M. Kontsevich. The Jacobian conjecture is stably equivalent to the Dixmier conjecture. Moscow Math. J. 7 (2007), 209–218.
9. S. Pinchuk. A counterexample to the strong real Jacobian conjecture. Mathematische Zeitschrift 217 (1994), 1–4.
10. SymPy Development Team. SymPy: Python library for symbolic mathematics. sympy.org.
11. Anonymous/AI-assisted note. An Explicit Counterexample to the Dixmier Conjecture in A₃. Omniscience Project, July 20, 2026. Unreviewed; concurrent work stating the same corollary without machine verification.

Appendix A  The Degree-Three Counterexample, in Full

Variables in order: x, y, z, a1, …, a19. Components Φ₁…Φ₂₂ of the map Φ : ℚ²² → ℚ²² (from degree3_counterexample.json; ** denotes exponentiation):

Φ1  = x − 3/2·x**2·y + a10·a9/2 + a10·x**2/2 + a9·x·z/2
Φ2  = y + 3·x·z + 12·x·y**2 + 3·a11·a9 + 3·a11·x**2 + 9·a12·a9 + 9·a12·x**2
      + 3·a13·a6 + 3·a13·y**2 − 3·a2·a3 + 3·a2·a9·x + 3·a3·a6·z − 9·a4·a6
      − 9·a4·y**2 + 9·a6·a9·y − 6·a8·a9 − 6·a8·x**2 − 6·a9·y·z
Φ3  = z + 4·y**2 + 3·x·y·z − a1·a2 + a1·a6·z − a14·a9 − a14·x**2 + 3·a15·a9
      + 3·a15·x**2 + 3·a16·a9 + 3·a16·x**2 − 7·a17·a6 − 7·a17·y**2 + 3·a18·a6
      + 3·a18·y**2 + a19·a6 + a19·y**2 + a2·a3·y + a3·a7 − 3·a4·a5 + 3·a4·a6·y
      − 3·a4·a8 − 3·a4·y·z + 3·a5·a9·y − 7·a6·x·y − a7·a9·x + 3·a8·a9·y
Φ4  = a1 − a17·a9 − a17·x**2 − a9·x·y
Φ5  = a2 + y**2·z
Φ6  = a3 + x**3
Φ7  = a4 + x**2·y
Φ8  = a5 + y**3
Φ9  = a6 + y**2
Φ10 = a7 + a2·y
Φ11 = a8 + y·z
Φ12 = a9 + x**2
Φ13 = a10 + x·z
Φ14 = a11 + a2·x
Φ15 = a12 + a6·y
Φ16 = a13 + a3·z
Φ17 = a14 + a7·x
Φ18 = a15 + a5·y
Φ19 = a16 + a8·y
Φ20 = a17 + x·y
Φ21 = a18 + a4·y
Φ22 = a19 + a1·z

Properties (all machine-verified): Φ = X + H, every term of H of degree 2 or 3 (68 monomials); det J_Φ ≡ 1; Φ(P₁) = Φ(P₂) = Φ(P₃) = (0, 0, −1/4, 0, …, 0) for the distinct rational points P₁, P₂, P₃ of Table 3. Note the transparent structure: components Φ₅–Φ₂₂ are the auxiliary "factor registers" (each of the form a_k + monomial), while Φ₁–Φ₄ carry the rewritten dynamics of Alpöge's map. A referee can check the collision by hand in Φ₅–Φ₂₂ (each auxiliary coordinate of P₂/P₃ is exactly minus its monomial's value) and verify Φ₁–Φ₄ with a few lines of CAS.

Appendix B  The Dixmier A₃ Witness

The endomorphism φ : A₃ → A₃ is given by φ(x_i) = F_i (the three polynomials of §2) and φ(∂_j) = Σ_k G_jk ∂_k, where G = adj(J_F)^T/(−2) ∈ M₃(ℚ[x, y, z]) (full entries in dixmier_witness_operators.txt, SHA-256 in Table 5). Machine-verified: G·J^T = I (canonical commutators [φ(∂_j), φ(x_i)] = δ_ij) and all 27 identities forcing [φ(∂_i), φ(∂_j)] = 0, each by full symbolic expansion to the literal zero polynomial, independently confirmed at 5 random rational points. Since A₃ is simple, φ is injective; since F is not injective on ℂ³, φ is not an automorphism (via [6, Ch. 10], [8]). Hence φ is an explicit injective, non-surjective endomorphism of A₃.