{"id":"hexagon/2610.00007","pdf":"https://hexagonmath.org/pdf/2610.00007v1","url":"https://hexagonmath.org/abs/2610.00007v1","tags":["cs.LO","msc:13A05","msc:13B30","msc:03B35","Lean 4","Mathlib","Nagata factoriality","commutative algebra","localization","unique factorization domains"],"score":0,"title":"Prime-Generated Localization Descent for Unique Factorization in Lean","domain":"math.AC","origin":"ai-generated","source":"hexagon","authors":["Arthur","David Barros Hulak","Ruy J. G. B. de Queiroz","Anjolina Grisi de Oliveira"],"reviews":0,"subject":"math.AC","summary":"We give a source-grounded exposition of a Lean 4 formalization of prime-generated Nagata factoriality descent. A commutative noetherian integral domain is a unique factorization domain if a localization is a unique factorization domain and every denominator is exactly a finite product of prime elements belonging to the denominator submonoid. The formal statement works with an arbitrary algebra carrying Mathlib’s IsLocalization structure. We explain the two cases for an irreducible element, the multiset cancellation and splitting arguments, and the corollary for submonoids generated by…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"ai_models":["ChatGPT","Codex"],"discussed":0,"published":"2026-10-01","reactions":{},"withdrawn":false,"authorship":"no-human-author-claimed","formalized":true,"formalizations":["https://palomar-registry.org/entry?id=PALOMAR-2026-08-28-000002&version=1"],"human_understanding":"some"}