The plane Jacobian conjecture

I am proving a theorem in Lean 4 and submitting it to Conjectura.

## Problem JC002 — The plane Jacobian conjecture

Does every polynomial map ℂ² → ℂ² with constant non-zero Jacobian determinant have a polynomial inverse? Open since 1939, and still open after the dimension-3 case was refuted in July 2026.

## Environment (fixed — do not assume anything newer)

- Lean toolchain: `leanprover/lean4:v4.33.0-rc1`
- Mathlib: `v4.33.0-rc1`

If a lemma you want does not exist in that Mathlib, prove it inline instead of
importing something newer.

## The exact statement I must prove

```lean
theorem solution : JacobianConjectureProp ℂ (Fin 2) := by
  sorry
```

## The file I submit

```lean
import Conjectura.Problems.JC002.Statement

namespace Submission

theorem solution : Conjectura.JC002.goal := by
  sorry

end Submission

```

## The Lean definitions of every term in this problem

These are the actual definitions your proof will be checked against. Do not
substitute your own version of any of them.

### Jacobian conjecture

The Jacobian conjecture for a ring `k` and index type `σ`: every `IsKellerMap` is an `IsPolynomialAutomorphism`. Open over a field of characteristic zero in every dimension above one.

```lean
Conjectura.AlgebraicGeometry.JacobianConjectureProp
-- unfolds to:
def JacobianConjectureProp (k σ : Type*) [CommRing k] [Fintype σ] [DecidableEq σ] : Prop :=
  ∀ F : RegularFunction k σ σ, IsKellerMap F → IsPolynomialAutomorphism F
```
Defined in this corpus.

### regular function

A regular function `k^σ → k^τ` is a tuple of multivariate polynomials, one per output coordinate. It is the formal stand-in for "polynomial map", and the object every statement in this area is about.

```lean
Conjectura.AlgebraicGeometry.RegularFunction
-- unfolds to:
abbrev RegularFunction (k : Type*) [CommRing k] (σ τ : Type*) := τ → MvPolynomial σ k
```
Defined in this corpus.

### Keller map

A Keller map is a polynomial self-map whose `RegularFunction.Jacobian` determinant is a unit. Over a field this is the same as the determinant being a non-zero constant, which is how the condition is usually stated.

```lean
Conjectura.AlgebraicGeometry.IsKellerMap
-- unfolds to:
def IsKellerMap {k σ : Type*} [CommRing k] [Fintype σ] [DecidableEq σ]
    (F : RegularFunction k σ σ) : Prop :=
  IsUnit F.Jacobian.det
```
Defined in this corpus.

### polynomial automorphism

A polynomial automorphism is a `RegularFunction` with a two-sided inverse that is itself a regular function. This is strictly stronger than being bijective on points: the inverse must be given by polynomials.

```lean
Conjectura.AlgebraicGeometry.IsPolynomialAutomorphism
-- unfolds to:
def IsPolynomialAutomorphism {k σ : Type*} [CommRing k]
    (F : RegularFunction k σ σ) : Prop :=
  ∃ G : RegularFunction k σ σ,
    G.comp F = RegularFunction.id k σ ∧ F.comp G = RegularFunction.id k σ
```
Defined in this corpus.

### Composition

Composition of regular functions, by polynomial substitution.

```lean
Conjectura.AlgebraicGeometry.RegularFunction.comp
-- unfolds to:
noncomputable def comp (F : RegularFunction k σ τ) (G : RegularFunction k τ ι) :
    RegularFunction k σ ι :=
  fun i => MvPolynomial.bind₁ F (G i)
```
Defined in this corpus.

### identity

The identity regular function: each coordinate is its own variable.

```lean
Conjectura.AlgebraicGeometry.RegularFunction.id
-- unfolds to:
noncomputable def id : RegularFunction k σ σ := MvPolynomial.X
```
Defined in this corpus.

### CommRing

class

```lean
CommRing
```
Defined in Mathlib.

### Fintype

class

```lean
Fintype
```
Defined in Mathlib.

### MvPolynomial

abbrev

```lean
MvPolynomial
```
Defined in Mathlib.

### IsUnit

def

```lean
IsUnit
```
Defined in Mathlib.

### det

def

```lean
F.Jacobian.det
```
Defined in Mathlib.

### bind

def

```lean
MvPolynomial.bind
```
Defined in Mathlib.

### X

def

```lean
MvPolynomial.X
```
Defined in Mathlib.

## Rules — submissions violating these are rejected automatically

1. **Do not change the name or type of `solution`.** It must satisfy the
   statement above exactly.
2. **Do not redefine or shadow anything from the problem's Statement module.**
   Declaring your own `goal`, or redefining a name it depends on, produces a
   proof of a *different* statement and is rejected. This is the single most
   common rejection.
3. **No `sorry`** anywhere, including in helper lemmas. It surfaces as the
   axiom `sorryAx` and is detected transitively through imports.
4. **No `native_decide`** — it surfaces as `Lean.ofReduceBool` and is not
   accepted, because it trusts compiled code rather than the kernel.
5. Only these axioms are permitted: `propext`, `Classical.choice`,
   `Quot.sound`.
6. Follow Mathlib style: hypotheses left of the colon, explicit types,
   `snake_case` theorem names, `UpperCamelCase` types.

## What I want from you

Here is my argument in informal mathematics:

> [PASTE YOUR PROOF SKETCH HERE]

Turn it into Lean 4 that compiles under the environment above and satisfies the
statement exactly. Where you are unsure a lemma exists in this Mathlib version,
say so explicitly rather than guessing a name.