{"id":"palomar/PALOMAR-2026-08-20-000001","url":"https://github.com/dcposch/jc2-lean/tree/3cee8100665bc59734511500b98728628ea190db/vertex-gap","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-20-000001-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 the vertex-gap obstruction at (k,d2) = (2,2) (label thm:22, Theorem 3.4 in the current compilation) from the campaign paper \"A Vertex-Gap Obstruction for Low-Degree Strip Pairs in the Plane Jacobian Conjecture\": for polynomials P, Q in K[x,y] over a field K of characteristic not in {2,3,5}, supported in the normalized type-(2,2) Newton strips along (1,2) with [P,Q] = x^2, the block coefficients satisfy a3 = 0 and a2^2*a6 = 0 - so the generic chart a2*a6 != 0 of the strip family is empty (VertexGap22, plus the side-symmetric companion VertexGap22_swapped in…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-20","reactions":{},"formalized":true,"formalizes":[{"title":"A Vertex-Gap Obstruction for Low-Degree Strip Pairs in the Plane Jacobian Conjecture (campaign paper, archived with its reproduction artifact \"Artifact for: A Vertex-Gap Obstruction for Low-Degree Strip Pairs in the Plane Jacobian Conjecture\")","identifier":"doi:10.5281/zenodo.21894922","relationship":"formalizes"}]}