The question of whether a given fixed Turing machine $M$ halts or not is something that can be independent of our fundamental axioms of mathematics.

For example, let $M$ be the Turing machine that searches for a proof of a contradiction from ZFC, say, halting only upon finding one. One could in principle write down the specific instructions for such a machine.

And in a universe in which ZFC is consistent, then $M$ never halts. But by the incompleteness theorem, if ZFC is consistent, then there are universes in which ZFC is true, but Con(ZFC) is false, and in such a universe, $M$ does halt.

Thus, the question of whether $s$ exists for a given machine $M$ that we can write down is something that can be independent of our axioms. And strengthening the theory doesn't really solve the problem, since the same argument will apply to the stronger theory.

More generally, although the collection of $n$-state programs that halt is a finite set, and therefore the halting times of the programs in this set is definitely bounded by some finite number, and we can easily prove that it is bounded, nevertheless the specific lower bounds that we can provide for how long the computations proceed will depend on our background theory.

The situation is that stronger and stronger theories may prove higher and higher lower bounds on the value of how long $n$-state programs can run while still halting.

So we can easily prove that $E_n$ exists, since it is determined by the set of $n$-state programs that halt and their running times. The thing we sometimes cannot prove is whether a given machine $M$ is in $E_n$ or not. A weak theory may not be able to prove that $M$ halts, even when a stronger theory is able to do so.

The question of whether a given fixed Turing machine $M$ halts or not is something that can be independent of our fundamental axioms of mathematics.

For example, let $M$ be the Turing machine that searches for a proof of a contradiction from ZFC, say, halting only upon finding one. One could in principle write down the specific instructions for such a machine.

And in a universe in which ZFC is consistent, then $M$ never halts. But by the incompleteness theorem, if ZFC is consistent, then there are universes in which ZFC is true, but Con(ZFC) is false, and in such a universe, $M$ does halt.

Thus, the question of whether $s$ exists for a given machine $M$ that we can write down is something that can be independent of our axioms. And strengthening the theory doesn't really solve the problem, since the same argument will apply to the stronger theory.

More generally, although the collection of $n$-state programs that halt is a finite set, and therefore the halting times of the programs in this set is definitely bounded by some finite number, and we can easily prove that it is bounded, nevertheless the specific lower bounds that we can provide for how long the computations proceed will depend on our background theory.

The situation is that stronger and stronger theories may prove higher and higher lower bounds on the value of how long $n$-state programs can run while still halting. No theory (computably axiomatized consistent) will be able to prove the optimal values for the busy beaver function, since if there were such a theory, then by searching for proofs we would be able to compute those values, which we provably cannot. So the stronger and stronger theories will continually settle additional halting instances pushing the values of the busy beaver function still higher.

So we can easily prove that $E_n$ exists, since it is determined by the set of $n$-state programs that halt and their running times. The thing we sometimes cannot prove is whether a given machine $M$ is in $E_n$ or not. A weak theory may not be able to prove that $M$ halts, even when a stronger theory is able to do so.