I think your question is not as precise as you portray it.
First, let me point out that you have not actually defined a
function $z$, in the sense of giving a first order definition of it in set theory, and you provably cannot do so, because of Tarski's theorem on the
non-definability of truth. We simply have no way to express the
relation x is definable in the usual first-order language
of set theory. More specifically:
Theorem. If ZFC is consistent, then there are models
of ZFC in which the collection of definable natural numbers
is not a set or even a class.
Proof. If V is a model of ZFC, then let $M$ be an internal
ultrapower of $V$ by a nonprincipal ultrafilter on
$\omega$. Thus, the natural numbers of $M$ are nonstandard
relative to $V$. The definable elements of $M$ are all
contained within the range of the ultrapower map, which in
the natural numbers is a bounded part of the natural
numbers of $M$. Thus, $M$ cannot have this collection of
objects as a set or class, since it would reveal to $M$
that its natural numbers are ill-founded, contradicting
that $M$ satisfies ZFC. QED
In such a model, your definition of $z$ is not first order. It could make sense to treat
your function $z$, however, in a model as an externally defined
function, defined outside the model (as via second-order
logic). In this case, other problems arise.
Theorem. If ZFC is consistent, then there is a model
of ZFC in which $f(n)\lt z(10000)$ for every natural number
n in the meta-theory.
Proof. If ZFC is consistent, then so is $ZFC+\neg Con(ZFC)$.
Let $V$ be a countable model of $ZFC+\neg Con(ZFC)+GCH$.
Since $V$ has no models of ZFC, the second part of your
definition is vacuous, and it reduces just to the
definability-in-$V$ part. Let $M$ be an internal ultrapower
of $V$ by an ultrafilter on $\omega$, so that $M$ is a
nonstandard version of $V$, with nonstandard natural
numbers. Let $N$ be a $V$-nonstandard natural number of
$M$. Every definable element of $M$ is in the range of the
ultrapower map, and therefore below $N$. In particular, for
every meta-theoretic natural number $n$, we have $f(n)\lt N$
in $M$, since $f(n)$ is definable. Now, let $M[G]$ be a
forcing extension in which the continuum has size
$\aleph_N^M$. Thus, $N$ is definable in $M[G]$ by a
relatively short formula; let's say 10000 symbols (but I
didn't count). Since the forcing does not affect the
existence of ZFC models or Turing computations between $M$
and $M[G]$, it follows that $f(n)\lt z(10000)$ in $M[G]$ for
any natural number of $V$. QED
Theorem. If ZFC is consistent, then there is a model
of ZFC with a natural number constant $c$ in which
$z(n)\lt f(c)$ for all meta-theoretic natural numbers $n$.
Proof. Use the model $M$ (or $M[G]$) as above. This time,
let $c$ be any $V$-nonstandard natural number of $M$. Since
the definable elements of $M$ all lie in the range of the
ultrapower map, it follows that every z(n), for
meta-theoretic $n$, is included in the $V$-standard
elements of $M$, which are all less than $c$. But $M$
easily has $c\leq f(c)$, and so $z(n)\lt f(c)$ for all these
$n$. QED
