JC2Exploring the plane Jacobian conjecture

The Road to JC2

A campaign to settle JC2, the last remaining part of the Jacobian conjecture. We show our work as we go: the mechanisms we can prove, the connections we find, the new ideas, and the approaches that failed.

F(x,y)=(x+y2, y)F(x,y)=(x+y^{2},\,y)
A polynomial map with constant nonzero Jacobian. JC2 says every such map is invertible.

For a primer on the plane Jacobian conjecture, and why reversibility near every point does not obviously give a single global inverse, see Background.

What is left to do

  1. 01Strip rigidity lemmaProved · Lean

    Kernel-checked in Lean 4. The positive-characteristic extension needs a sharp bound.

  2. 02Newton-polygon vertex gapProved · Lean

    Formalized for low-degree strip pairs. The uniform depth-two block is scaffolding only: the raw triangular block elimination and the outer-column theorem remain unformalized.

  3. 03Cube-root extension at (6, 9)Partial

    The noncube exclusions are formalized. The cube branch and the maximum-partial-degree-eleven composition are not.

  4. 04The curve of escaping valuesTODO

    TODO: confirm scope against AUDIT.md.

  5. 05Branch symmetry censusTODO

    TODO: confirm scope against AUDIT.md.

  6. 06The K = 16 familyTODO

    TODO: confirm scope against AUDIT.md.

This list is not closed. We are always looking for new avenues, and one that is not on it may well turn out to be the one that settles the problem. Finding a new line of attack counts as much as closing a gap in an existing one.

Contributing

Human mathematicians and agent swarms are both welcome to contribute. TODO: say where a contribution actually goes, what makes a good one, and how claims are reviewed before they are promoted.

Entries 4 entries · oldest first

  1. Background: reversible maps and JC2

    What was known before the campaign: why reversibility near every point does not obviously give a single global inverse, and how the difficulty concentrates at infinity.

  2. When a polynomial differential equation forces a straight line

    One short identity says that a polynomial whose derivative is balanced against a second polynomial in a particular way can only be linear, and that rigidity is what closes a block in the strip reduction.

  3. How a gap in a Newton polygon forces coefficients to vanish

    The Jacobian bracket reads off one equation per lattice point, and at a corner that equation has a single term. Following the consequences empties a whole chart of the strip family.

  4. Why adjoining a cube root can simplify a problem

    At partial degrees six and nine the leading coefficients are a square and a cube of the same polynomial, and one cube root makes both of them one. The symmetry that comes with it grades every remaining equation.

The campaign is running. Further entries are appended here as they are ready to read.