% Copyright 2026 Arthur Freitas Ramos, David Barros Hulak,
% Ruy J. G. B. de Queiroz, and Anjolina Grisi de Oliveira.
% Manuscript license: CC BY 4.0, https://creativecommons.org/licenses/by/4.0/
\documentclass[11pt]{amsart}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage[a4paper,margin=29mm]{geometry}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{microtype}
\usepackage{booktabs}
\usepackage{listings}
\usepackage{needspace}
\PassOptionsToPackage{obeyspaces,spaces}{url}
\usepackage{xurl}
\usepackage[hidelinks]{hyperref}
\hypersetup{pdftitle={Prime-Generated Localization Descent for Unique Factorization in Lean},
 pdfauthor={Arthur Freitas Ramos; David Barros Hulak; Ruy J. G. B. de Queiroz; Anjolina Grisi de Oliveira},
 pdfsubject={An exposition of a registered Nagata factoriality formalization},
 pdfkeywords={Nagata factoriality, localization, unique factorization, Lean, Mathlib}}
\emergencystretch=2em
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\newcommand{\PG}{\operatorname{PrimeGenerated}}
\newcommand{\Avoid}{\operatorname{Avoids}}
\newcommand{\im}{\iota}
\newcommand{\decl}[1]{{\small\nolinkurl{#1}}}
\newcommand{\source}[2]{\href{https://github.com/Arthur742Ramos/NagataFactoriality/blob/9ebcfa77a4f7eab6fdb663e7f151ceeb48abdff7/#1}{#2}}
\lstset{basicstyle=\ttfamily\footnotesize,columns=fullflexible,
 breaklines=true,breakatwhitespace=false,keepspaces=true,showstringspaces=false,
 aboveskip=10pt,belowskip=10pt,
 literate={∀}{{$\forall$}}1 {∈}{{$\in$}}1 {→}{{$\to$}}1
 {∃}{{$\exists$}}1 {∧}{{$\land$}}1}
\title[Prime-generated factoriality descent in Lean]{Prime-Generated Localization Descent for Unique Factorization in Lean}
\author{Arthur Freitas Ramos}
\author{David Barros Hulak}
\author{Ruy J. G. B. de Queiroz}
\author{Anjolina Grisi de Oliveira}
\thanks{Author ORCID identifiers: Arthur Freitas Ramos,
\href{https://orcid.org/0009-0003-3568-0325}{0009-0003-3568-0325};
David Barros Hulak,
\href{https://orcid.org/0009-0002-8056-1774}{0009-0002-8056-1774};
Ruy J. G. B. de Queiroz,
\href{https://orcid.org/0000-0003-1482-0977}{0000-0003-1482-0977}.}
\thanks{Copyright 2026 the authors. This manuscript is licensed under
\href{https://creativecommons.org/licenses/by/4.0/}{Creative Commons Attribution 4.0 International (CC BY 4.0)}.}
\date{October 1, 2026}
\subjclass[2020]{13A05, 13B30, 03B35}
\keywords{Nagata factoriality, prime-generated submonoid, localization, unique factorization domain, Lean 4, Mathlib}
\makeatletter
\def\shortauthors{A. F. Ramos, D. B. Hulak, R. J. G. B. de Queiroz, and A. G. de Oliveira}
\makeatother
\raggedbottom
\begin{document}
\begin{abstract}
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
\emph{IsLocalization} structure. We explain the two cases for an
irreducible element, the multiset cancellation and splitting arguments,
and the corollary for submonoids generated by arbitrary sets of primes.
A registered polynomial corollary illustrates reuse of the descent
package; its Laurent-polynomial premise is proved using Mathlib's
existing polynomial UFD instance, a dependency made explicit here.
The exposition is tied to the registered source and dependency pins,
distinguishes historical mechanical verification from manuscript review,
and situates the development relative to an earlier Lean preprint and
an Isabelle/HOL formalization. No new algebraic theorem or priority claim
is asserted.
\end{abstract}
\maketitle

\section{Introduction}

Localization simplifies algebra by turning selected elements into units.
The reverse passage is more delicate: factoriality of a localization need
not imply factoriality of the original domain. Nagata's criterion identifies
a useful situation in which it does. If the elements being inverted are
built out of prime elements, their effect on factorization can be tracked;
if the base domain also has factorization into irreducibles, primality can
be recovered before localization. Noetherianity supplies the latter
existence condition in the registered theorem considered here.

The classical mathematical source is Nagata's 1957 note
\cite{nagata1957}, specifically Lemma~2. That lemma assumes denominators
are products of prime elements of the ring. The formal artifact uses a
prime-generated submonoid condition that additionally requires each
chosen prime factor to belong to the denominator submonoid. The
elementwise proof discussed below closely follows the irreducibility and
primality transfer pattern also presented in the Stacks Project,
Tag~0AFU \cite{stacks}. Nagata's original proof and the present
implementation need not have identical intermediate objects to express
the same classical descent principle.

Our subject is the public Lean repository \cite{artifact} at commit
\decl{9ebcfa77a4f7eab6fdb663e7f151ceeb48abdff7}, registered as
\decl{PALOMAR-2026-08-28-000002}, version~1 \cite{palomar}.
The main purpose is to make the registered statements and their proof
dependencies readable without requiring the reader to reconstruct them
from Lean source. We give a mathematical proof of the implemented
descent argument, identify the corresponding declarations, and explain
the boundaries of the polynomial demonstration.

This is a new exposition of an existing formalization. The earlier Lean
preprint by Ramos, de Queiroz, and de Oliveira \cite{leanpreprint}
already treats this project. A related Isabelle/HOL development by
Ramos, Hulak, and de Queiroz appears in the Archive of Formal Proofs
\cite{afp}. These works are credited separately; the registered Lean
statements are not a verification of the earlier manuscript or of the
Isabelle session. Our contribution here is a precise account of the
pinned Lean artifact, including a dependency disclosure that matters
when interpreting its polynomial result.

\section{The registered mathematical statements}
\label{sec:statements}

Throughout the descent argument, $R$ is a commutative integral domain,
$S$ is a multiplicative submonoid of $R$, and $T$ is an $R$-algebra that
is a localization of $R$ at $S$. Write $\im:R\to T$ for the algebra map.
The notation $a/s$ denotes its localization fraction, not division in
$R$. When convenient we write $T=S^{-1}R$; the formal theorem does not
require $T$ to be the concrete quotient type bearing that name.

An element is irreducible when it is a nonunit and every factorization
has a unit factor. A prime element is nonzero, is a nonunit, and divides
one factor whenever it divides a product. A UFD is a domain in which
every nonzero nonunit factors into irreducibles and such factorizations
are unique up to associates and permutation. Mathlib packages the
multiplicative property as \decl{UniqueFactorizationMonoid}.

\subsection{Prime-generated denominators}

\begin{definition}\label{def:pg}
The submonoid $S$ is \emph{prime-generated} if, for every $s\in S$,
there is a finite multiset $f$ of elements of $R$ such that
\[
   s=\prod_{q\in f}q,
   \qquad q\in S\ \text{and}\ q\ \text{is prime for every }q\in f.
\]
The empty product is $1$. Define
\[
  \Avoid(S,p)\quad\Longleftrightarrow\quad
  (\forall s\in S)\ p\nmid s.
\]
\end{definition}

The multiset product counts occurrences, so repeated prime factors are
allowed. The factorization is an equality in $R$, not merely an equality
up to multiplication by a unit. The factors are prime elements, not
prime ideals, and their membership in $S$ is part of the condition.
There is no bound on the number of factors and no assumption that $S$
has finitely many generators. In particular, the finite product required
for each denominator must not be confused with finite generation of the
whole submonoid.

Definition~\ref{def:pg} has a direct set-theoretic interpretation.
If $P=\{q\in S:q\text{ is prime}\}$, then
\[
       \PG(S)\quad\Longleftrightarrow\quad S=\langle P\rangle,
\]
where $\langle P\rangle$ denotes multiplicative submonoid closure. Indeed,
the forward direction expresses each member of $S$ as a product of
members of $P$, and the reverse direction follows by closure induction.
This is an explanation of the predicate, rather than an additional
registered theorem.

Two consequences are worth keeping in view. First, $0\notin S$, because
every prime element is nonzero and a product of nonzero elements in a
domain is nonzero. Second, the only unit that can belong to such an $S$
is $1$: a nonempty product of nonunits cannot be a unit in a commutative
ring. Thus the predicate is more specific than a convention allowing
arbitrary unit factors in each displayed product. This causes no
difficulty for submonoids obtained as the closure of a set of primes.

\subsection{Descent and closure of prime generators}

\begin{theorem}[Registered Nagata descent]\label{thm:nagata}
Let $R$ be a commutative noetherian integral domain, let $S$ be a
prime-generated multiplicative submonoid, and let $T$ be a commutative
integral domain with an $R$-algebra structure making it a localization at
$S$. If $T$ is a UFD, then $R$ is a UFD.
\end{theorem}

This is \decl{NagataFactoriality.palomar_nagata_factoriality}.
The formal assumptions explicitly include the domain structure on both
$R$ and $T$. The latter is consistent with, and mathematically follows
from, localization of a domain at a submonoid avoiding zero; it remains
an explicit typeclass assumption in the selected statement. The
localization map is injective under these conditions. No embedding into
a particular fraction field is an additional input.

\begin{corollary}[Registered prime-generator specialization]
\label{cor:closure}
Let $R$ be a commutative noetherian integral domain, let $P\subseteq R$
consist of prime elements, and let $T$ be a commutative integral-domain
localization of $R$ at $\langle P\rangle$. If $T$ is a UFD, then $R$ is
a UFD.
\end{corollary}

The declaration is
\decl{NagataFactoriality.palomar_nagata_factoriality_of_prime_generators}.
To obtain it, use closure induction to prove $\PG(\langle P\rangle)$.
A generator is represented by a singleton multiset, $1$ by the empty
multiset, and multiplication by multiset addition. Every resulting
factor belongs to the closure because it began as a generator. Then
apply Theorem~\ref{thm:nagata}. The set $P$ is arbitrary, including the
empty set; in the empty case the localization inverts only $1$ and the
descent is tautological. The repository also supplies finite-generator
and powers-of-a-prime wrappers outside the three selected declarations.

\subsection{Where noetherianity enters}

The proof of primality of irreducibles in Section~\ref{sec:proof} needs
no noetherian hypothesis. Noetherianity enters when assembling those
lemmas into a UFD structure: Mathlib provides a
\decl{WfDvdMonoid R} instance for a noetherian domain, giving termination
of descent by proper divisibility and hence factorization existence.
The project wrapper \decl{hasFactorization_of_noetherian} is an
\decl{infer_instance} invocation, not a new proof of the noetherian
factorization theorem.

The closing characterization says that well-founded divisibility together
with primality of every irreducible yields a UFD. In the source,
\decl{ufd_of_factorization_and_primes} packages this step through
Mathlib's prime-factor characterization. It is important not to replace
this explanation by the false equivalence ``a domain is a UFD if and
only if it is noetherian and every irreducible is prime.'' Noetherianity
is sufficient here, but not necessary for a domain to be a UFD. The
registered theorem retains it as its chosen factorization hypothesis.

\section{The elementwise proof}
\label{sec:proof}

We now prove Theorem~\ref{thm:nagata} in the form implemented by the
prime-generated branch of
\source{NagataFactoriality/Nagata/Lemmas.lean}{\decl{Nagata/Lemmas.lean}}.
All cancellation below takes place in the integral domain $R$.
Products of prime elements are nonzero, so each cancellation used in
the argument has an explicit nonzero justification.

\subsection{Clearing denominators}

The localization interface supplies the following facts:
\begin{align}
  &\text{every }z\in T\text{ can be written as }a/s,
       &&a\in R,\ s\in S,\label{eq:surj}\\
  &a/s=b/t\quad\Longleftrightarrow\quad at=bs,
       &&s,t\in S,\label{eq:cross}\\
  &\im(a)\mid\im(b)\quad\Longleftrightarrow\quad
       \exists s\in S\ (a\mid sb).\label{eq:dvd}
\end{align}
For the forward implication of \eqref{eq:dvd}, write a quotient witness
as $c/s$ and cross-multiply to obtain $sb=ac$. Conversely, if $sb=ac$,
then $c/s$ is a quotient witness for divisibility in $T$. Equation
\eqref{eq:cross} uses injectivity of the map from $R$; for a general
ring localization an additional multiplier from $S$ would occur.
The domain and zero-exclusion assumptions are what allow the simplified
cross-product equality here.

These statements occur in the abstract helper namespace
\decl{NagataFactoriality.IsLocalization}, as
\decl{surj}, \decl{mk'_eq_iff}, and \decl{dvd_map_iff}.
Elements of $S$ map to units, and fractions with unit numerators are
units. The helper interface derives these results from Mathlib's
localization API.

\subsection{An irreducible divisor of a prime product}

\begin{lemma}\label{lem:hit}
If $p$ is irreducible and divides a finite product of prime elements,
then $p$ is prime.
\end{lemma}
\begin{proof}
Induct on the number of factors. The empty product is $1$, which an
irreducible cannot divide. For a product $qv$, write $qv=pd$, with $q$
prime. Since $q\mid pd$, either $q\mid p$ or $q\mid d$.
In the first case, irreducibility of $p$ and of $q$ implies that they
are associates, so $p$ is prime. In the second case write $d=qe$ and
cancel the nonzero element $q$ to obtain $v=pe$. The induction
hypothesis applies to the remaining prime factors.
\end{proof}

The implemented result is
\decl{prime_of_irreducible_of_dvd_prime_factors}, and its
submonoid specialization is
\decl{prime_of_irreducible_of_dvd_mem_primeGenerated}.
Consequently, an irreducible $p$ that divides even one denominator is
already known to be prime before any appeal to factoriality of $T$.

\subsection{Cancellation of denominators avoiding an irreducible}

\begin{lemma}\label{lem:cancel}
Let $p$ be irreducible, let $f$ be a multiset of prime elements, and
suppose $p\nmid q$ for every $q\in f$. If
\[
             \Bigl(\prod_{q\in f}q\Bigr)a=pc,
\]
then $p\mid a$.
\end{lemma}
\begin{proof}
Induct on $f$. With no factors the assertion is immediate. Write the
product as $qv$. Primality of $q$ gives $q\mid p$ or $q\mid c$.
If $q\mid p$, the two irreducibles are associates, contradicting
$p\nmid q$. Therefore $c=qe$. Cancel $q$ from $qva=pqe$ and apply
the induction hypothesis to $va=pe$.
\end{proof}

This is \decl{dvd_of_mul_eq_prime_factors}. Notice that the argument
does not assume that $p$ is prime: that is precisely what the final
descent proof is trying to establish.

\begin{corollary}\label{cor:reflect}
If $\PG(S)$, $p$ is irreducible, and $\Avoid(S,p)$, then
\[
          \im(p)\mid\im(a)\quad\Longrightarrow\quad p\mid a.
\]
\end{corollary}
\begin{proof}
By \eqref{eq:dvd}, $p\mid sa$ for some $s\in S$. Expand $s$ as its
prime-factor multiset. No factor can be divisible by $p$, since every
factor belongs to $S$ and $p$ avoids $S$. Lemma~\ref{lem:cancel}
removes those factors.
\end{proof}

The corresponding abstract declaration is
\decl{dvd_of_localization_dvd_primeGenerated_isLocalization}.
The avoidance hypothesis is essential to this reflection result: an
element being inverted can divide every localized element without
dividing each numerator in the original ring.

\Needspace{13\baselineskip}
\subsection{Splitting a denominator product between two numerators}

\begin{lemma}\label{lem:split}
Suppose $f$ is a multiset of prime elements and
\[
            p\Bigl(\prod_{q\in f}q\Bigr)=ab.
\]
There are multisets $f_1,f_2$ and elements $a',b'\in R$ with
\begin{align*}
    f_1+f_2&=f, &a&=\Bigl(\prod_{q\in f_1}q\Bigr)a',\\
    p&=a'b', &b&=\Bigl(\prod_{q\in f_2}q\Bigr)b'.
\end{align*}
\end{lemma}
\begin{proof}
Induct on $f$. For the empty multiset use $a'=a$, $b'=b$.
For a leading prime $q$, the equality shows $q\mid ab$, so $q$ divides
$a$ or $b$. Remove it from that numerator, cancel it from the equality,
and use the induction hypothesis for the remaining multiset. Add the
removed occurrence of $q$ to the corresponding part of the partition.
\end{proof}

The source theorem \decl{split_prime_factors_of_mul_eq} includes an
irreducibility parameter for $p$, named \decl{_hp}; its induction does
not use that parameter. Irreducibility becomes necessary in the next
lemma. Multisets record both the partition and the multiplicities,
avoiding a choice of ordering of the denominator factors.

\begin{lemma}\label{lem:irred}
If $\PG(S)$, $p$ is irreducible in $R$, and $\Avoid(S,p)$, then
$\im(p)$ is irreducible in $T$.
\end{lemma}
\begin{proof}
If $\im(p)$ were a unit, it would divide $1$. Equation \eqref{eq:dvd}
would give $p\mid s$ for some $s\in S$, contradicting avoidance.
Now suppose $\im(p)=xy$. Write $x=a/s$ and $y=b/t$ using
\eqref{eq:surj}. Cross multiplication yields $p(st)=ab$.
Express $st$ as a prime-factor multiset and apply
Lemma~\ref{lem:split}. Since $p=a'b'$ is irreducible, either $a'$ or
$b'$ is a unit. If $a'$ is a unit, then
\[
            x=\im\Bigl(\prod_{q\in f_1}q\Bigr)(a'/s)
\]
is a product of units: its first factor comes from $S$, and $a'/s$
has unit numerator. The case of $b'$ is symmetric. Thus every
factorization of $\im(p)$ has a unit factor.
\end{proof}

The implementation is
\decl{localization_irreducible_of_irreducible_primeGenerated_isLocalization}.
Unlike the divisibility-reflection proof, it explicitly manipulates
fraction representatives. The requirement that each prime factor of a
denominator belongs to $S$ is used when proving that the two partition
products map to units.

\subsection{The two cases and the UFD conclusion}

\begin{proof}[Proof of Theorem~\ref{thm:nagata}]
Let $p$ be irreducible in $R$. If $p$ divides some $s\in S$,
Lemma~\ref{lem:hit} shows that $p$ is prime. Otherwise
$\Avoid(S,p)$ holds. Lemma~\ref{lem:irred} makes $\im(p)$
irreducible in $T$ and hence prime because $T$ is a UFD.

If $p\mid ab$ in $R$, map the divisibility to $T$. Primality of
$\im(p)$ gives $\im(p)\mid\im(a)$ or $\im(p)\mid\im(b)$.
Corollary~\ref{cor:reflect} brings the selected divisibility back to
$R$. Together with the nonzero and nonunit conditions from
irreducibility, this proves that $p$ is prime in the second case too.
Finally, noetherianity supplies factorization into irreducibles, and
the UFD characterization completes the proof.
\end{proof}

The source separates the last primality reflection into
\decl{prime_of_localization_prime_primeGenerated_isLocalization}
and assembles the case split in
\decl{nagata_key_lemma_primeGenerated_isLocalization}.
The top-level descent theorem then supplies noetherian factorization
and invokes this key lemma for every irreducible.

\section{Lean interfaces and proof architecture}
\label{sec:lean}

Lean~4 \cite{lean4} and Mathlib \cite{mathlib} supply the ring,
submonoid, localization, and factorization infrastructure. The project
organizes its additional proof into a small wrapper layer and the
transfer lemmas described above. The three registered declarations use
ordinary Mathlib types; their statement module does not import the
project-specific definition $\PG$.

\subsection{The selected statement surface}

The following display transcribes the type of the first selected
declaration from \source{Challenge.lean}{\decl{Challenge.lean}},
with line wrapping adjusted for display.
The theorem body is omitted; its proved counterpart occurs in
\source{Solution.lean}{\decl{Solution.lean}}.
\begin{lstlisting}
theorem palomar_nagata_factoriality
    {R T : Type*} [CommRing R] [IsDomain R]
    [IsNoetherianRing R]
    (S : Submonoid R) [CommRing T] [Algebra R T]
    [_root_.IsLocalization S T] [IsDomain T]
    (hS : ∀ s : R, s ∈ S →
      ∃ f : Multiset R,
        (∀ q ∈ f, q ∈ S ∧ Prime q) ∧ f.prod = s)
    (hUFD : UniqueFactorizationMonoid T) :
    UniqueFactorizationMonoid R
\end{lstlisting}
The source is linked above. In particular,
the conjunction in $hS$ requires both membership and primality for
each occurrence in the multiset.

The proof body of this declaration is a single application of
\decl{nagata_theorem_isLocalization}. The prime-generator declaration
uses \decl{Submonoid.closure s} in its localization assumption and
the premise that every member of $s$ is prime. Its solution invokes
\decl{nagata_theorem_of_prime_generators_isLocalization}, which uses
the closure lemma described in Corollary~\ref{cor:closure}.
The polynomial declaration is
\begin{lstlisting}
theorem palomar_polynomial_ufd
    {R : Type*} [CommRing R] [IsDomain R]
    [IsNoetherianRing R] [UniqueFactorizationMonoid R] :
    UniqueFactorizationMonoid R[X]
\end{lstlisting}
Its solution calls
\decl{polynomial_uniqueFactorizationMonoid_via_nagata}.
The mathematical dependence of that call is discussed in
Section~\ref{sec:polynomial}.

\subsection{Abstract and concrete localization}

The principal prime-generated transfer lemmas are stated at the abstract
\decl{IsLocalization S T} level. This allows the key argument to work
directly in a ring such as a Laurent-polynomial ring once its localization
instance is supplied. The proof does not first transport everything to
the concrete quotient \decl{Localization S}. Concrete theorem names
are also provided, but specialize the abstract transfer lemmas.

For the concrete localization, the zero-exclusion fact is installed
locally as a \decl{Fact} instance asserting $0\notin S$, so that typeclass search can
recover the domain structure. For the abstract selected theorem,
\decl{IsDomain T} is already a hypothesis; zero exclusion is still
derived from $\PG(S)$ when an injectivity or cross-multiplication
helper needs it. These are interface choices and should not be read as
additional mathematical restrictions hidden outside the displayed
statement.

The module boundary follows the argument. \decl{Basic/Noetherian.lean}
and \decl{Basic/UFD.lean} supply factorization existence and final UFD
assembly. \decl{Localization/IsLocalization.lean} supplies the abstract
fraction interface. \decl{Nagata/Lemmas.lean} contains the multiset
inductions and transfer chain, while \decl{Nagata/Theorem.lean} exposes
abstract, concrete, and generator-based descent statements. The
application layer and \decl{Solution.lean} then select the public result.
These module paths are relative to \decl{NagataFactoriality/}, except
for the root solution module.

\subsection{The prime-or-unit variant}

The repository retains another chain under the hypothesis
\[
        (\forall s\in S)\quad s\text{ is prime or a unit}.
\]
This condition is excessively restrictive for a multiplicative
submonoid of a domain. In fact it permits no nonunits. If a nonunit
$p\in S$ existed, it would be prime; closure would give $p^2\in S$.
The square is not a unit and cannot be prime, because prime implies
irreducible and $p^2=p\cdot p$ has two nonunit factors. This
contradicts the condition.

Accordingly this variant does not cover even the powers of one prime.
It is logically valid as a descent statement, but inverts units only,
so the localization has not changed the ring up to isomorphism. The
three registered declarations use prime-generated denominators
instead. The powers-of-$X$ application depends on allowing $X^2$ and
higher products, exactly as Definition~\ref{def:pg} does. The
distinction is about the scope of the hypothesis, not a counterexample
to the truth of a proved theorem.

\section{The polynomial specialization and its dependencies}
\label{sec:polynomial}

The third registered result says that $R[X]$ is a UFD when $R$ is a
commutative noetherian integral domain carrying a UFD structure. The
result is classical and already follows from Mathlib's polynomial
factorization instance without the noetherian assumption. Its role in
this artifact is to exercise the localization-descent interface.

\subsection{Conditional descent from Laurent polynomials}

Let $A=R[X]$ and $S=\{X^n:n\geq0\}$. The polynomial $X$ is prime
when $R$ is a domain, and its powers form a prime-generated submonoid:
represent $X^n$ by $n$ copies of $X$. Mathlib identifies the Laurent
ring $R[X,X^{-1}]$ as a localization of $A$ away from $X$.
Noetherianity of $R$ supplies noetherianity of $A$ through the
polynomial-ring infrastructure. Thus Theorem~\ref{thm:nagata} gives
the useful conditional implication
\[
   R[X,X^{-1}]\text{ is a UFD}\quad\Longrightarrow\quad
   R[X]\text{ is a UFD}.
\]
The source packages this as
\decl{polynomial_uniqueFactorizationMonoid_of_laurent}.
This step really is an application of the descent theorem and does not
assume a UFD structure on $R[X]$.

\subsection{How the registered proof supplies the premise}

To prove the Laurent premise from a UFD structure on $R$, the source
uses \decl{laurentPolynomial_uniqueFactorizationMonoid}. Its first
line installs the existing Mathlib instance:
\begin{lstlisting}
letI : UniqueFactorizationMonoid R[X] := inferInstance
\end{lstlisting}
This is a substantive mathematical dependency. The remainder represents
a nonzero Laurent polynomial, after multiplication by a unit monomial,
as an ordinary polynomial $p$. It removes the largest power of $X$
dividing $p$, leaving a nonzero polynomial $q$ not divisible by $X$.
It then factors $q$ using the UFD structure on $R[X]$ just installed.
Each prime factor not associated to $X$ remains prime in the Laurent
ring, using localization of its principal prime ideal. The monomial
factors become units, and the prime factorization gives the Laurent
UFD structure.

Finally,
\decl{polynomial_uniqueFactorizationMonoid_via_nagata}
uses this Laurent structure and calls the conditional descent theorem.
The full dependency path is therefore
\[
\begin{gathered}
  \text{Mathlib polynomial UFD instance for }R[X]\\
  \Longrightarrow\text{the project's Laurent UFD construction}\\
  \Longrightarrow\text{Nagata descent back to }R[X].
\end{gathered}
\]
This is a sound proof term, because the initial UFD instance is already
proved in the imported library. It is not an independent derivation
of polynomial factoriality avoiding that theorem. The distinction
does not affect the type or validity of the registered corollary; it
does affect what methodological contribution should be attributed to
its proof. The pinned Mathlib file
\decl{Mathlib/RingTheory/Polynomial/UniqueFactorization.lean}
contains \decl{Polynomial.uniqueFactorizationMonoid}, with no
noetherian-ring premise. The pinned library also provides
\decl{UniqueFactorizationMonoid.of_isLocalization}, a general forward
transfer of UFD structure to a localization. Thus Laurent factoriality
is not an absent library capability; the project gives an explicit
construction using available factorization and localization infrastructure.

\subsection{A separate constant-prime construction}

The repository also includes
\source{NagataFactoriality/Applications/FractionField.lean}{\decl{Applications/FractionField.lean}},
which is not the proof selected by \decl{palomar_polynomial_ufd}.
It localizes $R[X]$ at the closure of the constant polynomials $C(r)$
with $r$ prime in $R$. These constant polynomials are prime, so the
denominator submonoid is prime-generated. Since $R$ is a UFD, every
nonzero coefficient is associated to a finite product of primes. Its
constant image therefore becomes a unit in this localization.

This lets the source identify the localization with
$\operatorname{Frac}(R)[X]$, by comparing both as localizations at the
larger submonoid of nonzero constant polynomials. The polynomial ring
over the fraction field obtains a UFD instance from Mathlib, and that
instance is transported across the algebra equivalence before descent.
This path has a different dependency structure from the Laurent
demonstration: it invokes polynomial factoriality over a field in the
localized ring. We describe it as a companion construction in the
source, not as an additional registered declaration or a new algebraic
result. Likewise, the iterated polynomial wrapper in
\decl{Applications/Laurent.lean} reuses the selected construction; it
does not remove its library dependency.

\section{Prior work and provenance}
\label{sec:provenance}

Nagata's note \cite{nagata1957} establishes the classical factoriality
criterion; the registered artifact's metadata also names
\emph{Local Rings} and Samuel's \emph{Lectures on Unique
Factorization Domains} as background. Our elementwise presentation
has been reconstructed from the pinned Lean proof and is not a
reproduction of textbook prose. The Stacks Project
\cite{stacks} makes explicit that factorization existence can be
separated from localization transfer, matching the logical division
used here. Its criterion is broader than the noetherian selected
statement in the factorization hypothesis.

The April 2026 preprint \cite{leanpreprint} discusses the same Lean
project under an earlier toolchain. Its authors are Arthur F. Ramos,
Ruy J. G. B. de Queiroz, and Anjolina Grisi de Oliveira. It is prior
exposition of this formalization, not evidence that the August
registered source has precisely the same declarations, hypotheses,
or dependency graph. The present account uses the August pin and
explicitly states the polynomial overlap documented in
Section~\ref{sec:polynomial}. It does not retain any first-public-
formalization claim.

The AFP entry \cite{afp}, dated April 20, 2026, credits Arthur Freitas
Ramos, David Barros Hulak, and Ruy Jose Guerra Barretto de Queiroz.
It formalizes prime-generated factoriality descent in Isabelle/HOL,
using record-based ring and localization interfaces and depending on
the AFP entry \emph{The Localization of a Commutative Ring}. It
also packages closure-based corollaries and polynomial-localization
applications. This is related work with a different prover and
interface, rather than an outcome checked by the Lean registration.
The Lean repository includes Isabelle files, but those files are
outside the registered Lean statement surface and the verification
scope discussed next.

The attribution of a manuscript, a formalization artifact, and a
registry submission are separate matters. The pinned Palomar record
lists Arthur Freitas Ramos, David Barros Hulak, and Ruy J. G. B. de
Queiroz for the registered artifact, with Arthur as responsible
maintainer. Credit to the earlier Lean manuscript includes de
Oliveira as indicated above. No inference about which author proved
an individual lemma is made from these lists.

\section{Registered verification and reproducibility}
\label{sec:verification}

\subsection{Exact source identity}

The record \cite{palomar} fixes Lean
\decl{leanprover/lean4:v4.33.0} and Mathlib commit
\decl{db584cd6d46c92f209a44c0f1c829460d327499d}.
The repository commit is
\decl{9ebcfa77a4f7eab6fdb663e7f151ceeb48abdff7}.
These identities distinguish the registered artifact from the
Lean~4.24.0 snapshot described by the earlier preprint. Reproducing
the selected result means checking the pinned source and lock file,
not the current repository branch or a PDF alone.

The registry records a successful mechanical verification at
August 27, 2026, 23:55:51 UTC, with registration on August 28,
2026, 01:12:18 UTC. Its linked workflow is
\href{https://github.com/PalomarRegistry/PalomarSubmission/actions/runs/33127679460}{run 33127679460}.
The archived mechanical report \cite{mechanical} has status
\decl{pass}, no report-level errors or warnings, and SHA-256
\decl{dc1fae6a07a45cf6e5c65a6777635a6266302ec10d35809d8d0bd6bbe6ffbc57}.
The retained compilation log does contain expected statement-placeholder
warnings and style-linter warnings; a report-level pass is not a claim
that the historical Lean compiler output was warning-free.

\subsection{Statement and proof separation}

The statement-only module \decl{Challenge.lean} imports four
Mathlib modules and contains three intentional \decl{sorry}
placeholders. It fixes the target types using only ordinary library
definitions. The separate module \decl{Solution.lean} provides proved
declarations with the same names by invoking the project theorems.
The registration compares this pair; the statement placeholders are
not evidence that the selected solution proofs rely on an admitted
result. Conversely, searching source text for placeholders is not a
substitute for the statement comparison and axiom check.

The recorded permitted axioms are \decl{propext},
\decl{Quot.sound}, and \decl{Classical.choice}. These are the
standard classical and quotient foundations of this Lean development.
Thus ``no additional project axioms'' is the appropriate interpretation;
the result is not an axiom-free constructive proof. The record's
preservation metadata also archives the project and pinned dependencies.

The solution and challenge SHA-256 values in the record are,
respectively,
\decl{e3a673c72a1935a2ebe45651ec24b4596f5886e98a314555ee345ea8d221bc3b}
and
\decl{76dd7103a3fc14ea71e25a6f494930dd56217971e2ed83cb6f89b66680181d25}.
They provide byte-level identifiers in addition to the repository commit.
The verification is historical evidence for those selected statements;
the preparation of this manuscript did not rerun Lean, Comparator,
or NanoDa.

\subsection{A reproduction boundary}

A reader can retrieve the pinned repository, install the recorded Lean
toolchain, retain its \decl{lake-manifest.json}, fetch the Mathlib
cache with \decl{lake exe cache get}, and compile the selected proof
module and its dependencies with \decl{lake build Solution}. A project-wide
\decl{lake build} checks the configured library targets. Replaying
the registration's statement comparison and exported-term verification
additionally requires the recorded external tool versions; ordinary
project compilation should not be represented as the same operation.

Neither the mechanical registration nor this exposition establishes
that a manuscript is free of every explanatory error, that a theorem
is new, or that a human referee has reviewed it. The formal target
types still need to match the intended mathematical claim. This is why
the precise denominator condition and the polynomial dependency have
been emphasized independently of the pass result.

\subsection{AI assistance and author understanding}

The pinned formalization metadata describes manual mathematical
development and OpenAI Codex assistance for repository preparation,
statement/proof separation, and reproducibility checks. It does not
identify a precise historical model version for every proof task.
This historical description is separate from the present manuscript.

This manuscript was drafted primarily with GPT-6.1 assistance,
including source cross-checking and typesetting. The submitting
author, Arthur Freitas Ramos, reports understanding some parts of
the work. This statement does not assert full understanding by him
or any level of understanding by the other named manuscript authors.
AI-assisted mathematical and source review is not independent human
peer review. The Lean source is licensed Apache-2.0; the manuscript
and its TeX source are licensed CC BY 4.0. The manuscript license
does not relicense the formalization, its dependencies, or the cited
prior works.

\section{Conclusion}

The registered development separates Nagata descent into a
factorization-existence input and an elementwise prime-transfer
argument. Finite prime-factor multisets serve two different purposes:
they cancel denominators in divisibility reflection and partition
denominator factors in irreducibility preservation. The abstract
localization interface lets the same chain apply to different
representations of a localization, while closure induction supplies
the prime-generator corollary without a finite-generation restriction.

The polynomial declaration is best understood as a demonstration of
this interface within an existing algebra library. Its selected
Laurent proof depends on Mathlib's polynomial UFD instance and makes
no independent-proof claim. Broader denominator conventions,
nonnoetherian generalizations, and ideal-theoretic class-group
formulations are outside the three selected statements. An extension
in any of these directions would need its own explicit statement,
proof, and verification evidence.

\bibliographystyle{amsplain}
\bibliography{references}
\end{document}