Candidates on proved false arithmetic statements Questions
Are there any known proved pure existence arithmetic statements? I.e. statements of the form $\exists n P(n)$, for which no upper bound on $n$ is known? If yes, is there some where the predicate expressed by $P(n)$ is computable (i.e. $\exists n P(n)$ is $\Sigma_1^0$ statement)? Is there some as in the first question proved in ZFC and independent of PA? Is there some required AC?
Motivation
The questions are motivated by the problem of arithmetical soundness of ZFC. While arithmetical soundness of PA is doubtless, I'm not so sure about ZFC. The evidence for the former is given by real physical implementation of natural numbers via ordinary counting, which is surely satisfies PA axioms. On the contrary, ZFC reasons about infinite entities, for which such evidence can not be provided. And ZFC proves more arithmetical statements, than PA does ($\mathrm{Con}_{\mathrm{PA}}$ and Paris-Harrington theorem are examples). So, it is a possibility that some of them false, even if ZFC is consistent. It's also related to Hilbert's conservation program.
This conclusion is sad, but I've got a worse one. If ZFC is consistent and arithmetically sound, then it is impossible even to prove the implication $\mathrm{Con}_{\mathrm{ZFC}}\rightarrow \mathrm{ArithmSnd}_{\mathrm{ZFC}}$, where $\mathrm{ArithmSnd}_{\mathrm{ZFC}}$ denotes some internal formalization of arithmetical soundness. I'm not diving into details of how exactly it is defined, but I feel ZFC can formalize this concept, at least because it has the model theory machinery. For my argument the exact definition is not important. What is important is that $\mathrm{ArithmSnd_{ZFC}}$ internally implies that proved to be provable statements are indeed provable, namely $\mathrm{ZFC}\vdash \mathrm{ArithmSnd_{ZFC}}\rightarrow (\Box\Box\varphi\rightarrow\Box\varphi)$, where $\varphi$ is an arithmetical statement and $\Box$ denotes provability in ZFC. Also, according to this answer, the latter is equivalent to arithmetical $\Sigma_1^0$-soundness. In particular, $\mathrm{ArithmSnd_{ZFC}}\rightarrow(\Box\Box\bot\rightarrow\Box\bot)\rightarrow(\neg\Box\bot\rightarrow\neg\Box\Box\bot)\leftrightarrow(\mathrm{Con_{ZFC}}\rightarrow\neg\Box\neg\mathrm{Con_{ZFC}})$, where $\bot$ denotes a contradiction.
So assume ZFC consistent is arithmetically sound and $\mathrm{ZFC}\vdash \mathrm{Con_{ZFC}}\rightarrow \mathrm{ArithmSnd_{ZFC}}$. Then
$$
\mathrm{ZFC}\vdash \mathrm{Con_{ZFC}}\rightarrow \neg\Box\neg\mathrm{Con_{ZFC}}\\
\mathrm{ZFC}\vdash\mathrm{Con_{ZFC}}\rightarrow \mathrm{Con_{ZFC+Con_{ZFC}}}\\
\mathrm{ZFC}+\mathrm{Con_{ZFC}}\vdash \mathrm{Con_{ZFC+Con_{ZFC}}}.
$$
By the second incompleteness theorem, the latter means $\mathrm{ZFC}+\mathrm{Con_{ZFC}}$ is inconsistent, and taking into account the assumption of ZFC consistency, it gives $\mathrm{ZFC}\vdash\neg\mathrm{Con_{ZFC}}$, which contradicts the arithmetical soundness assumption.
As a result, the situation is similar to that with consistency. If ZFC is consistent and arithmetical sound, then there is no hope to prove the implication $\mathrm{Con}_{\mathrm{ZFC}}\rightarrow \mathrm{ArithmSnd}_{\mathrm{ZFC}}$ someday. But, as was mentioned, if ZFC is arithmetically unsound, there exist provable arithmetically false statements, even if it's consistent. And pure existence results are candidates on such statements: ZFC proves $\exists nP(n)$, but in reality such $n$ doesn't exist. So I'm wondering if any such "suspicious" proved results are known.
 A: I believe there is no upper bound on TREE(3) that is expressible in a more concrete way than by referring back to the TREE function.   The fact that TREE(3) exists is expressible by a $\Sigma^0_1$ sentence $(\exists n)\text{TREE}(3,n)$ with parameter $3$.  
The fact that TREE($m$) exists for all $m$ is not "suspicious" in my opinion, but the sequence does grow very quickly. See (1) for some info on the TREE sequence and see (2) for this claim:

Theorem (Friedman). TREE(3) is greater than the halting time of any Turing machine
  initialized with a blank tape, which can be proved to halt in $\text{ACA}_{0} + \Pi^1_2\text{-BI}$ by a proof with at most $2^{1000}$ symbols.

Here BI refers to Bar Induction. The point is that if we had any "nice" upper bound, presumably we would be able to print out the result with a Turing Machine and prove that the machine halts using a reasonable number of symbols.  Note that the theorem does not require us to prove that the upper bound is an upper bound, only to construct a machine that prints the upper bound and prove that the machine eventually halts.
Regarding later parts of the question: it is true that ZFC proves more arithmetical sentences than PA. But PA proves every true $\Sigma^0_1$ sentence, so these can never be independent of PA. What tends to happen, as in TREE, is that there is a hidden parameter: e.g. for each $m$, PA proves $(\exists n)\text{TREE}(\dot m, n)$, but PA doesn't prove $(\forall m)(\exists n)\text{TREE}(m, n)$. 
ZFC and ZF prove the same arithmetical sentences, so the axiom of choice is not relevant. 
A: As described here you can construct over any practical $Σ_1$-sound formal system $S$ a sentence $Q$ such that $S$ proves $Q$ and also that ( if $S$ is $Σ_1$-sound then $Q$ is true but whose shortest proof over $S$ has at least on the order of $2^{10000}$ symbols ). However, I can say with complete confidence that you can never encode or verify any such proof, because it is far too long for the observable universe!
So the answer to your question is yes! Observe that $S$ proves that ( $S$ proves $Q$ ), which is a mere $Σ_1$-sentence that is true in the real-world if $S$ is $Σ_1$-sound, but if you believe that $S$ is $Σ_1$-sound then you must believe that there is no real-world proof of $Q$ over $S$!
The only way out would be if $S$ is not $Σ_1$-sound, but we all want to believe that our foundational system for mathematics is $Σ_1$-sound! So either we have to give up our belief that our foundational system is sound, or we have to accept that it proves an existential sentence that has no real-world witness.
In any case, the very notions of "formal system" and "consistency", not to say "$Σ_1$-soundness", all essentially rely on the (abstract) collection of all finite binary strings or something equivalent, so in some sense it will no longer make sense to ask your question once you accept my claim that the real world does not have an exact embedding of a model of PA. I do not know of any viable way around that...
