Can you clarify what you mean by BBλ being "provably optimal"? IIUC BB functions for any Turing-complete computation model should be equivalent up to a constant. Maybe something like: there exists N, c: forall n >= N: BBλ(n) < BB(n + c) and vice-versa. I am not sure what the exact equation will be off-hand, maybe in this case we will need to replace BB() with a version based on binary encoding of TMs.
tromp|1 year ago
> for any other busy beaver BB based on self-delimiting programs, there is a constant c such that a(c+n) >= BB(n)
This requires an information theoretic measure of program size, such as bits or bytes, whereas the TM-based BB measures in states. I don't believe there are additively tight bounds on how many states are needed to encode an arbitrary string of n bits.