That might affect your proving power but it won't affect the Turing Machine itself. That Turing Machine either will or will not halt after the given number of steps, regardless of whether or not you "hand it" the CH or not. To change the result of BB requires not a change of how you are approaching the proof but the behavior of the TMs themselves, but the TMs are well-defined. Regardless of the computability of the number, BB(10,000,000) is a particular number, regardless of what proof system you try to approach it with.

Amusingly, this opens up the distinct possibility of a wrong proof. You take the CH as an axiom, or, perhaps more likely, some other attractive axiom more relevant to the task at hand, and you "prove" a result with that axiom, but then you never find out that your proof is wrong and in fact the TM's behavior is other than what you proved, because... how are you supposed to run a TM for 10^10^10^10^10^10^10^10^10^10^10^10^10^10^10 steps to check your proof anyhow? (Especially since that number would be the tiniest insignificant baby steps for the BB(7) winner.)

Again, if you want to change the BB number, you need to change the Turing Machines themselves, most commonly by adding an oracle to them to result in BB*.

But that's not what OP said and you're stating something that is very different. OP said the following:

"I'm not sure whether ZFC+CH could have a different idea about BB(8000) than ZFC+notCH would."

And the answer to that is yes, it's in principle possible that ZFC+CH contains a proof that a given TM halts after N steps while ZFC+notCH contains a proof that said TM does not halt after N steps. If that were the case and assuming that both are consistent it will be the case that said TM does not in fact halt (period) and that ZFC+notCH uses a model of non-standard arithmetic in its proof.

You mention the possibility of a wrong proof, but that is mixing up the notion of proof and truth which are not the same things. The proofs in ZFC+notCH and ZFC+CH are both correct since a proof is nothing more than a syntactic structure that adheres to certain rules. It's that ZFC+notCH is using a model of natural numbers that is not what most people normally consider to be a natural number, it's using a model of natural numbers that admits for the possibility of incredibly large numbers that are larger than any ordinary/standard natural number. In effect ZFC+CH would contain a proof that after some unimaginably large number of steps the Turing machine halts whereas ZFC+notCH does not allow for the existence of numbers that large.

So the main concept here is that two formal systems may have different notions of what a natural number is. We humans share some idea of what a natural number is supposed to be and we call those the standard natural numbers but the problem is that there is no formal way to precisely pin down those numbers without also allowing for the possibility of bizarre non-standard natural numbers as well. In this hypothetical case we would conclude that ZFC+notCH comes closer to modelling what we consider the actual natural numbers compared to ZFC+CH, but nevertheless it's impossible for any first order formal system to fully specify the natural numbers and only the natural numbers.

Again, in order to affect the TM's execution time, the "proof difference" must have a first step where your TM with CH takes a different step than the one without CH does. There can be no such first step. There is no room in the TM specification for that. It doesn't matter what you prove or don't prove, the TM "with CH" and the TM "without CH" must take the exact same steps.

You are messing up proof vs. truth. Your proof doesn't affect how long a TM runs for. Your axioms do not affect how long the TM runs for. Show me, in the state table of the TM, where the CH or any other axiom you use for analysis affects the truth table or the execution time of the TM. No amount of analysis can change how many steps a TM runs for. The numbers may be large, but they are finite and completely determined. The only thing it can affect is whether you can know the number, but the number exists regardless.

Even more concretely: Show me how your choice of axioms affects BB(4). Show me how it affects the number of steps, without redefining BB. Forget CH; take any axiom you like... for the analysis. Just don't affect the TM itself; that's a given for you. Take anything else you like and show me how it changes the BB(4) number. You can't. You can easily take axioms that will produce a wrong result; most notably we could just take as an axiom that BB(4) = -4. The resulting analysis will show that BB(4) is -4. It will also be wrong.

I am confident my explanation addresses OPs original question, which is whether two different (and consistent) formal systems can disagree about whether a given TM halts or not (and hence differ about what the value of BB(N) for some N), and the answer is yes they can. The source of that disagreement would come down to two different models of natural numbers where the theory that proves that a given TM halts only models non-standard natural numbers whereas the theory that proves that the given TM does not halt contains a standard model of the naturals.

What you're discussing is a completely different matter that while is interesting, does not address OP's issue and is something I already responded to by stating that one must be very careful to differentiate between what is actually true versus what can be proven by a formal system. You are blurring the lines between the two but that distinction is critical to understanding the point being made.

I'm the OP. That was exactly my question, great explanation. I've been confused by similar apparent paradoxes before, where I didn't clearly distinguish something being true inside the theory and outside of it.