PoissonConjecture.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

11 declarations, 6 contain sorry, 0 declared as axioms

The Poisson Conjecture

References:

[AvdE07] arxiv/math.0608009 On the equivalence of the Jacobian, Dixmier and Poisson Conjectures in any characteristic by Kossivi Adjamagbo, Arno van den Essen. Published as A proof of the equivalence of the Dixmier, Jacobian and Poisson conjectures, Acta Math. Vietnam. 32 (2007), 205–214.
[BCW82] The Jacobian conjecture: reduction of degree and formal expansion of the inverse by Hyman Bass, Edwin H. Connell, David Wright, Bull. Amer. Math. Soc. 7 (1982), 287–330.
[Alp26] Counterexample to the Jacobian conjecture by Levent Alpöge (2026), disproving the Jacobian conjecture in dimension $3$
[Lon26] An Explicit Counterexample to the Rank-Two Poisson Conjecture by Christopher D. Long (2026), disproving $PC_2$

The Poisson Conjecture $PC_n$ ([AvdE07], Notations 5) asserts that, over a field of characteristic zero, every endomorphism of the n-th canonical Poisson algebra $P_n(K)$ — the polynomial algebra $K[X_1, \dots, X_{2n}]$ equipped with the canonical Poisson bracket — is an automorphism.

By [AvdE07], Theorem 7 (the "United Conjectures Theorem"), for every n there is a chain of implications $$JC_{2n} \Longrightarrow PC_n \Longrightarrow DC_n \Longrightarrow JC_n,$$ where $JC_n$ is the Jacobian Conjecture in dimension n and $DC_n$ the Dixmier Conjecture for the n-th Weyl algebra (the implication $DC_n \Longrightarrow JC_n$ being classical [BCW82]). Since the Jacobian conjecture was disproved in dimension $3$ [Alp26] — and hence in every dimension $n ≥ 3$ by padding with identity coordinates — $PC_n$ is false for all $n ≥ 3$: composing the counterexample's failure of $JC_3$ through $PC_3 \Longrightarrow DC_3 \Longrightarrow JC_3$ refutes $PC_3$, and directly, the cotangent (symplectic) lift of the counterexample map ([AvdE07], Theorem 1 in reverse) is a non-invertible Poisson endomorphism of $P_3(K)$. $PC_2$ is false as well, by the explicit rank-two counterexample of [Lon26]. Only $n = 1$ remains open.

Indexing note: we index the $2n$ variables of $P_n(K)$ by Fin n ⊕ Fin n, with Sum.inl i playing the role of $X_i$ and Sum.inr i the role of $X_{i+n}$ of [AvdE07], so that the canonical bracket reads $\{X_i, X_{i+n}\} = 1$; see MvPolynomial.poissonBracket.

Imports (2)

def Arxiv.«math.0608009».IsPoissonEndomorphism Documented declaration: IsPoissonEndomorphism line 73 source
Source documentation
A K-algebra endomorphism φ of the polynomial algebra in $2n$ variables is an endomorphism of the n-th canonical Poisson algebra $P_n(K)$ if it preserves the canonical Poisson bracket. Following [AvdE07], Lemma 2, it is equivalent to require preservation on the generators only, which is the form used here (the brackets of generators are constants, so preserving and intertwining them agree).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Nat, AlgHom, MvPolynomial, Sum, Fin, Finsupp
Proof uses: Eq, MvPolynomial.poissonBracket, MvPolynomial.X
25 instances, coercions and auxiliary constants left out.
```
def IsPoissonEndomorphism {n : ℕ}
    (φ : MvPolynomial (Fin n ⊕ Fin n) K →ₐ[K] MvPolynomial (Fin n ⊕ Fin n) K) : Prop :=
…
```
def Arxiv.«math.0608009».PoissonConjectureFor The Poisson Conjecture in dimension n ($PC_n$ in the notation of [AvdE07]): every endomorphism of the n-th canonical Poisson algebra over K is an automorphism line 82 source
Source documentation
The Poisson Conjecture in dimension n ($PC_n$ in the notation of [AvdE07]): every endomorphism of the n-th canonical Poisson algebra over K is an automorphism. An endomorphism is an automorphism iff it is bijective, since the inverse of a bijective algebra endomorphism preserving the Poisson bracket is again such.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Nat
Proof uses: AlgHom, MvPolynomial, Sum, Fin, Finsupp, Arxiv.«math.0608009».IsPoissonEndomorphism, Function.Bijective
12 instances, coercions and auxiliary constants left out.
```
def PoissonConjectureFor (n : ℕ) : Prop :=
…
```
theorem Arxiv.«math.0608009».poisson_conjecture Documented declaration: poisson_conjecture sorry line 94 source
Source documentation
The Poisson Conjecture ([AvdE07], the characteristic zero case): for every n, every endomorphism of the n-th canonical Poisson algebra over a field K of characteristic zero is an automorphism. This is false: the Jacobian conjecture fails in dimension $3$ [Alp26], hence so does $PC_3$ (via [AvdE07], Theorem 7, or directly via the symplectic lift of the counterexample map).

depends on sorry what this means
Statement uses: Field, CharZero, Not, Nat, Arxiv.«math.0608009».PoissonConjectureFor
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem poisson_conjecture : ¬ ∀ n, PoissonConjectureFor K n := by
…
```
Mentions: Arxiv.«math.0608009».PoissonConjectureFor
theorem Arxiv.«math.0608009».poisson_conjecture.variants.dimension_one The Poisson Conjecture in dimension $1$ ($PC_1$) is open sorry line 104 source
Source documentation
The Poisson Conjecture in dimension $1$ ($PC_1$) is open. By [AvdE07], Theorem 7, it is implied by the Jacobian conjecture in dimension $2$ (Keller's original problem, open) and implies the Dixmier conjecture for the first Weyl algebra (Problem 1 of Dixmier (1968), open).

depends on sorry what this means
Statement uses: Field, CharZero, Arxiv.«math.0608009».PoissonConjectureFor, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem poisson_conjecture.variants.dimension_one : PoissonConjectureFor K 1 := by
…
```
Mentions: Arxiv.«math.0608009».PoissonConjectureFor
theorem Arxiv.«math.0608009».poisson_conjecture.variants.dimension_two The Poisson Conjecture is false in dimension $2$ ($PC_2$) sorry line 123 source
Source documentation
The Poisson Conjecture is false in dimension $2$ ($PC_2$). [Lon26] gives four explicit polynomials $R, T, D, S \in \mathbb{Q}[x, q, p, z]$ with $\{R, D\} = \{T, S\} = 1$ and $\{R, T\} = \{R, S\} = \{D, T\} = \{D, S\} = 0$, so that $X_1 \mapsto R$, $X_2 \mapsto T$, $X_3 \mapsto D$, $X_4 \mapsto S$ is a Poisson endomorphism of $P_2(K)$. It is not surjective: in the coordinates $(X_1, X_2, X_3, X_4)$ the two rational points $(0, 0, 1/24, -1/8)$ and $(1, 2/3, 247/96, -89/64)$ have the same image under $(R, T, D, S)$, so every polynomial in the image of the endomorphism takes equal values at them, while $X_1$ does not. The formulas have rational coefficients and the two points are rational, so the argument applies over every field of characteristic zero.
This does not settle any conjecture further down the chain of [AvdE07], Theorem 7, which only propagates falsity upwards: $\lnot PC_2$ gives $\lnot JC_4$, already known from [Alp26]. $DC_2$, $JC_2$ (Keller's problem), $PC_1$ and $DC_1$ all remain open.

depends on sorry what this means
Statement uses: Field, CharZero, Not, Arxiv.«math.0608009».PoissonConjectureFor, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem poisson_conjecture.variants.dimension_two : ¬ PoissonConjectureFor K 2 := by
…
```
Mentions: Arxiv.«math.0608009».PoissonConjectureFor
theorem Arxiv.«math.0608009».poisson_conjecture.variants.dimension_three The Poisson Conjecture is false in dimension sorry line 136 source
Source documentation
The Poisson Conjecture is false in dimension $3$: the cotangent (symplectic) lift $\Phi(X_i) = F_i$, $\Phi(X_{i+3}) = \sum_j M_{ij} X_{j+3}$ with $M = (JF)^{-\top}$ of the degree-$6$ counterexample map $F$ of [Alp26] (whose Jacobian determinant is the constant $-2$, so $M$ is a polynomial matrix) is a Poisson endomorphism of $P_3(K)$ that is not injective on points — e.g. it identifies $(0, 6, -142, 0, 0, 0)$ and $(1, 0, 2, 0, 0, 0)$ — and is therefore no automorphism. Alternatively, $PC_3$ fails by [AvdE07], Theorem 7, as it implies the Jacobian conjecture in dimension $3$, contradicting [Alp26].

depends on sorry what this means
Statement uses: Field, CharZero, Not, Arxiv.«math.0608009».PoissonConjectureFor, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem poisson_conjecture.variants.dimension_three : ¬ PoissonConjectureFor K 3 := by
…
```
Mentions: Arxiv.«math.0608009».PoissonConjectureFor
theorem Arxiv.«math.0608009».poisson_conjecture.variants.dimension_ge_two The Poisson Conjecture is false in every dimension $n ≥ 2$, by padding the dimension $2$ counterexample of [Lon26] with identity canonical pairs sorry line 144 source
Source documentation
The Poisson Conjecture is false in every dimension $n ≥ 2$, by padding the dimension $2$ counterexample of [Lon26] with identity canonical pairs.

depends on sorry what this means
Statement uses: Field, CharZero, Nat, LE.le, OfNat.ofNat, Not, Arxiv.«math.0608009».PoissonConjectureFor
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem poisson_conjecture.variants.dimension_ge_two (n : ℕ) (hn : 2 ≤ n) :
    ¬ PoissonConjectureFor K n := by
…
```
Mentions: Arxiv.«math.0608009».PoissonConjectureFor
theorem Arxiv.«math.0608009».poisson_conjecture.variants.jacobian_implication The Jacobian conjecture in dimension $2n$ implies the Poisson conjecture in dimension n ([AvdE07], Theorem 1 and Theorem 7) sorry line 153 source
Source documentation
The Jacobian conjecture in dimension $2n$ implies the Poisson conjecture in dimension n ([AvdE07], Theorem 1 and Theorem 7).

depends on sorry what this means
Statement uses: Field, CharZero, Nat, JacobianConjecture.JacobianConjectureProp, Fin, HMul.hMul, OfNat.ofNat, Arxiv.«math.0608009».PoissonConjectureFor
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
20 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem poisson_conjecture.variants.jacobian_implication (n : ℕ)
    (h : JacobianConjectureProp K (Fin (2 * n))) : PoissonConjectureFor K n := by
…
```
Mentions: Arxiv.«math.0608009».PoissonConjectureFor
theorem Arxiv.«math.0608009».isPoissonEndomorphism_id The identity is a Poisson endomorphism line 162 source
Source documentation
The identity is a Poisson endomorphism.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Nat, Arxiv.«math.0608009».IsPoissonEndomorphism, AlgHom.id, MvPolynomial, Sum, Fin, Finsupp
Proof uses: of_eq_true, Eq, MvPolynomial.poissonBracket, MvPolynomial.X, eq_self
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem isPoissonEndomorphism_id (n : ℕ) :
    IsPoissonEndomorphism (AlgHom.id K (MvPolynomial (Fin n ⊕ Fin n) K)) := by
…
```
Mentions: Arxiv.«math.0608009».IsPoissonEndomorphism
theorem Arxiv.«math.0608009».poissonBracket_X_pairing The canonical bracket pairs each position variable with its momentum variable line 170 source
Source documentation
The canonical bracket pairs each position variable with its momentum variable.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Nat, Fin, Eq, MvPolynomial, Sum, MvPolynomial.poissonBracket, MvPolynomial.X, Sum.inl, Sum.inr, OfNat.ofNat, Finsupp
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, ite, MvPolynomial.poissonBracket_X_inl_inr, ite_cond_eq_true, eq_self
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem poissonBracket_X_pairing (n : ℕ) (i : Fin n) :
    poissonBracket (X (Sum.inl i) : MvPolynomial (Fin n ⊕ Fin n) K) (X (Sum.inr i)) = 1 := by
…
```
theorem Arxiv.«math.0608009».poissonConjectureFor_zero The Poisson conjecture holds trivially in dimension $0$, where the Poisson algebra is K itself and the identity is the only endomorphism line 178 source
Source documentation
The Poisson conjecture holds trivially in dimension $0$, where the Poisson algebra is K itself and the identity is the only endomorphism.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Arxiv.«math.0608009».PoissonConjectureFor, OfNat.ofNat, Nat
Proof uses: AlgHom, MvPolynomial, Sum, Fin, Finsupp, Arxiv.«math.0608009».IsPoissonEndomorphism, Eq, AlgHom.id, MvPolynomial.algHom_ext, Sum.elim, MvPolynomial.X, Fin.elim0, Eq.mpr, Function.Bijective, id, congrArg, Function.bijective_id
14 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem poissonConjectureFor_zero : PoissonConjectureFor K 0 := by
…
```
Mentions: Arxiv.«math.0608009».PoissonConjectureFor