What would it mean for BB(n) to "not exist"? Recall that BB(n) is defined in a very concrete way: you take all the Turing machines of size n (which are easily enumerable combinatorial objects), remove ones which do not halt, then take the largest runtime of the ones that are left. Since we can always write down a Turing machine which halts immediately, we know that there's a trivial lower bound for each BB(n), and since the Turing machines are deterministic, we know that any machine that halts must do so in a fixed number of steps. With such a straightforward construction, it's hard to see how such a number could "not exist," at least not without appealing to an ontology somewhat outside of the mainstream (e.g. ultrafinitism).
> So you can remove the ones that do not halt by inspecting them one by one and developing a specific algorithm for each one that determines if it halts or not.
Is impossible. You can’t, in general, inspect Turing machines one-by-one to determine if they halt.
Trivially a non-halting program for any n exists. Also trivially there must be some non-halting program with the highest number of steps.
We can’t necessarily find that program, but there is almost by definition some non halting program with the highest number of steps
That isn't trivial. Whether a given program halts might be independent of ZFC, or of any consistent logical system you might try to use. The question of whether such a program "really" halts is one which might not have an answer. ZFC claims there must be an answer, because LEM, but why should we care what ZFC or first order logic or anything has to say on the matter, if they can't actually tell us whether it halts?
It's not a constructive proof, you don't need to give a process.
It's trivial to construct a candidate for each n, which gives a lower bound.