Delphi.science

The Jacobian conjecture in dimension 2n implies the Poisson conjecture in dimension n

Source: github.com/zblore/fc-jacobian-poisson/tree/e395ab52d16b1c26…

Zayn Blore

Palomar Registrypalomar/PALOMAR-2026-11-03-000028Nov 3, 2026math.RAscore 0

A machine-checked proof that, over a field of characteristic zero, the Jacobian conjecture in dimension 2n implies the Poisson conjecture in dimension n (K. Adjamagbo and A. van den Essen, 2007, Theorem 7). The statement and definitions are Formal Conjectures' (poisson_conjecture.variants.jacobian_implication in PoissonConjecture.lean, arXiv math/0608009), copied verbatim into Challenge.lean, so this entry proves Formal Conjectures' own statement. A Poisson endomorphism's Jacobian matrix lies in Mathlib's symplectic group, so its determinant is a unit; the Jacobian conjecture then gives a…

RepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-11-03-000028
curl -X POST /api/v1/records/palomar/PALOMAR-2026-11-03-000028/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-11-03-000028/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'