{"id":"palomar/PALOMAR-2026-09-09-000001","url":"https://github.com/itpplasma/global-stafford-formal/tree/e676caed1253e5d09fc6699d5dc683febbabf7bb","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-09-000001-v2.json","repo":"https://github.com/itpplasma/global-stafford-formal","tags":["math.RA","math.AG","msc:16S32","msc:14F10","ring-theory","differential-operators","algebraic-geometry","lean"],"score":0,"title":"Global Stafford","trust":"high","domain":"math.RA","source":"palomar","authors":["Christopher Albert"],"reviews":0,"subject":"math.RA","summary":"Lean formalization of the same-divisor identity 1 = d*R + F*d*S in the ring of k-linear finite-order differential operators of every smooth integral finitely generated algebra over a characteristic-zero field, extending Stafford's Conjecture 3.8 from Weyl algebras to smooth affine varieties.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-09","reactions":{},"formalized":true}