>It's easy to see that the largest such value is an upper bound on BB(745), but even that isn't worth much.

Having an upper bound on the value of a BB(N) is all you need to solve BB(N). Why? Because if you have an upper bound called U, then you know that any Turing Machine that runs for more than U steps will run forever. So an upper bound is as good as a solution.

>There could be an infinite number of such values.

No there can't be an infinite number of these because the number of 745 state Turing Machines is finite and each Turing Machine represents one possible value for what BB(N) can be. The number of possible binary Turing Machines with N states is 6 * (N + 1) ^ (3 * N).

As for the rest of your post, I think to address it we should step back from busy beavers and just focus on one specific aspect of it that is easier to reason about.

Let's say there's some Turing Machine H, and whether H halts is independent of ZFC, that is ZFC is unable to prove whether H halts or runs forever. Does this mean that in fact H can both halt and not halt depending on our interpretation? Is it possible that H both halts and does not halt? Can we as humans just decide to choose one axiomatic system where H halts, or we can decide to choose another axiomatic system where H does not halt and both systems are perfectly valid and legitimate?

Of course not. If whether H halts or runs forever is independent of ZFC, then in fact H never halts. It's not a matter of personal choice, or a matter of interpretation, or something we can just arbitrarily choose, H simply runs forever.

We can tell from outside of ZFC that H must run forever, even though from inside of ZFC the proposition is unprovable. That does not mean that ZFC is able to prove that H halts; what it means is that ZFC is unable to precisely define what a natural number is and that from inside of ZFC there are two possible systems of natural numbers:

In one system of natural numbers H runs forever, which is the system of natural numbers that corresponds to the actual truth. This system of natural numbers is what we call the standard model of arithmetic and is the intended interpretation of the natural numbers [1].

In another system of natural numbers, the nonstandard model of arithmetic, H halts after X steps where X is a nonstandard natural number [2]. You can think of a nonstandard natural number as a number that is larger than any standard natural number, for example imagine a whole number with an infinite number of digits. Now we know that a natural number is only supposed to have a finite number of digits, but ZFC is not powerful enough to define natural numbers this way, so it can not eliminate every model of natural numbers that have infinite digits and in one such model H does halt.

In fact, no consistent first order system is powerful enough to define natural numbers in such a way that they only have a finite number of digits, every single first order system will have some model of natural numbers that have an infinite number of digits.

So no, the fact that HALT(H) is independent of ZFC does not mean that we can just decide to pick an axiomatic system where H halts or one where it does not halt and both are valid choices, because in the system where H halts we are no longer working with the actual natural numbers. It's only in the axiomatic system where H never halts that we get to work with the natural numbers.

Given these concepts, you can now apply them to better understand how the busy beaver function can only have one single value. Yes there are propositions of ZFC where BB(745) = n1, and BB(745) = n2, and both of these propositions are independent of ZFC. No, that does not mean that BB(745) can actually be either n1 or n2 and the choice is a matter of preference. Only one axiomatic system represents the actual natural numbers, and the other ones represent the nonstandard natural numbers whose values can be infinitely large and have infinitely many digits.

[1] https://en.wikipedia.org/wiki/Interpretation_(logic)#Intende...

[2] https://en.wikipedia.org/wiki/Non-standard_model_of_arithmet...