It has been proven that BB(745) is independent of ZFC (Johannes Riebel, 2023). Many experts believe that this will be true of BB(k) for values of k much smaller than 745 (some people say 15, 20, or even 10).
Now my understanding is that ZFC can always prove that a Turing Machine M will halt, if indeed it does halt. The difficulty comes when M does not halt, and ZFC has to prove that. (Per Gödel's theorem, there will be a non-halting Turing Machine T that is undecidable from ZFC (assuming ZFC is consistent))
But then why can't ZFC come up with the value of BB(745)? After all, the 745-state BB is a halting Turing Machine (by definition of Busy Beaver), and we have established that ZFC can always prove that a TM halts, if indeed it does. So why can't ZFC have a proof of the value of BB(745)?
An answer that comes to mind is that there is a difference between ZFC proving that 745-state BB halts (which ZFC can do), and ZFC having a proof of the value of BB(745) (which ZFC cannot do). Is that distinction accurate and answers my question?
Any feedback would be appreciated. Thanks!