Computational algebraic analysis proves degree-minimality of Alpöge's counterexample to the Jacobian conjecture, demonstrating rigidity in low-degree equivariant Keller maps.
Key Points
To determine whether Alpöge's degree-7 counterexample to the Jacobian conjecture is degree-minimal within its equivariant class on complex three-space.
Classified C*-equivariant Keller maps using exact rational arithmetic and automated degree searches.
Generated and cross-checked Gröbner-basis certificates using msolve and Singular.
Machine-verified general quotient identities across parameter families in the Lean 4 interactive theorem prover.
Demonstrated that every C*-equivariant Keller map of total degree at most 6 for weight systems (−1,1,2), (−1,1,3), and (−1,1,4) is a polynomial automorphism, confirming Alpöge's degree-7 example is degree-minimal.
Formally verified the quotient identity det Dφ = −Ek det JF in Lean 4 for all k ≥ 2.