A proof in HA of statements like $\forall m\forall x (\exists y T(m,x,y) \vee \neg\exists y T(m,x,y))$ is, in itself, not enough to extract recursive functions solving unsolvable problems (which would show that such statements are not provable in HA).

It has been suggested that this somehow follows from the disjunction and existence properties (DP, EP) of HA (see François' comment), however one can only apply DP and EP on *closed* statements, while statements like the one above have a prefixing $\forall m \forall x \cdots$.

That is why in recursive realizability (Kleene number realizabilty), that extracts recursive functions from intuitionistic arithmetic proofs, one must assume a version of the formal arithmetical Church's Thesis like CT$_0$: $\forall x\exists y A(x,y) \to \exists e\forall x\exists u (T(e,x,u)\wedge A(x,U(u))$, that allows to transform the $\forall\exists$-quantifier-alternation from $\forall m\forall x\exists z ((z=0\to\exists y T(m,x,y)) \wedge (z\neq 0 \to \neg\exists y T(m,x,y)))$ into a $\exists\forall$-one. *Now*, as the result is a closed statement one can apply EP to extract a recursive function solving an unsolvable problem.

However, the last argument would just show that the original statement is not provable in HA+CT$_0$ while being provable in PA -- ignoring the fact that $\neg$CT$_0$ is provable in PA.

Indeed, the statement $\neg$CT$_0$ is an example of a statement provable in PA, but not provable in HA. The latter follows from existence of models of HA refuting CT$_0$ (for ex. PA itself).

On the other hand, a *natural* statement was demanded in the original question, and I am not sure $\neg$CT$_0$ is so natural.