The minimal equivariant counterexample to the Jacobian conjecture

Machine-certified classification of C*-equivariant Keller maps on C3. We prove that Alpöge's degree-7 counterexample to the Jacobian conjecture is degree-minimal within its full equivariant class: every C*-equivariant Keller map of total degree at most 6 for weights (−1,1,2) is a polynomial automorphism. The same rigidity holds through degree 6 for weight systems (−1,1,3) and (−1,1,4). For every k ≥ 2 and weights (−1,1,k) we prove the quotient identity det Dφ = −Ek det JF, machine-checked in Lean 4 uniformly in k, which drives the equivariant degree search across the family. All computations are exact (rational arithmetic). Gröbner-basis certificates (msolve, cross-checked in Singular) accompany the paper.