A Dimension-Two Counterexample to the Separable Jacobian Conjecture in Characteristic Two
Romy Mondello
math.AG
Jul 29, 2026 · v1
math.AC
TL;DR
An appendix records a Lean formalization verifying parts of the characteristic-two counterexample to the separable Jacobian conjecture.
Abstract
Let k be the algebraic closure of F_2. We study the polynomial endomorphism F=(P,Q) of the affine plane, where P=x+x^2 y+x^4+x^6 y^2 and Q=y+x^5+x^6 y+x^7 y^2+x^8 y^3. Its Jacobian determinant is 1, while the three distinct points (0,1), (1,0), and (1,1) have the same image. We prove that [k(x,y):k(P,Q)]=3 and that the extension is separable. Thus the generic degree is prime to the characteristic although F is not an automorphism, giving a dimension-two counterexample to the separable Jacobian conjecture in characteristic two. The proof uses explicit recovery from a hidden cubic, irreducibility over the actual target field, and a bridge between function-field embeddings and the geometric generic fiber. We also give an explicit graph presentation proving that F is etale and derive the map from a coordinate-permuted form of a three-variable map of Irit Huq-Kuruvilla. An appendix records the precise scope and evidence boundaries of a Lean formalization and an independent Harmonic Aristotle replay.
Problem
The separable (Adjamagbo) Jacobian conjecture asks whether a polynomial endomorphism with unit Jacobian and generic degree prime to the characteristic must be an automorphism. Whether counterexamples exist in dimension two and characteristic two was open.
Approach
An explicit plane map F=(P,Q) over the algebraic closure of F_2 is analyzed. The authors recover the source function field from a hidden cubic element, prove irreducibility of its minimal polynomial over the actual target field k(P,Q), and establish separability. A graph presentation shows F is étale, and a pullback bijection identifies the geometric generic fiber points with field embeddings. An appendix documents the scope of a Lean formalization and an independent Harmonic Aristotle replay.
Results
F has Jacobian determinant 1 and is étale, but three distinct points share an image, so it is not an automorphism. The extension k(x,y)/k(P,Q) has separable degree 3, prime to the characteristic, giving a dimension-two counterexample to the separable Jacobian conjecture in characteristic two.
