{"id":"palomar/PALOMAR-2026-08-19-000005","url":"https://github.com/dcposch/jc2-lean/tree/6c0f56309226432afb90b6213638ec987d46f4a3/theorem-a","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-19-000005-v1.json","repo":"https://github.com/dcposch/jc2-lean","tags":["math.AG","math.AC","msc:14R15","algebraic-geometry","jacobian-conjecture","lean-formalization"],"score":0,"title":"dcposch/jc2-lean","trust":"high","domain":"math.AG","source":"palomar","authors":["Dan Clemens Posch"],"reviews":0,"subject":"math.AG","summary":"Lean 4 / Mathlib formalization of Theorem A (ODE rigidity, all weights; label thm:ode, Theorem 6.1 in the current compilation of the campaign paper): if polynomials A, C over an integral domain of characteristic zero and an integer weight nu >= 1 satisfy A*C' - nu*A'*C = c for a nonzero constant c, then deg A <= 1 (TheoremA). Also a standalone positive-characteristic strengthening extracted from the same proof (TheoremA_charP): the same conclusion over a domain of characteristic p under the degree bounds nu*deg A < p and deg C < p. The theorem is the rigidity engine of the depth-two block…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-19","reactions":{},"formalized":true,"formalizes":[{"title":"Sheet-number obstruction theory for the plane Jacobian Conjecture: campaign theory bundle v1","identifier":"doi:10.5281/zenodo.22002825","relationship":"formalizes"}]}