Some comments:
The length of that proof grows with the number of symbols needed to represent the number N within program A
Program A needs F(N), not on N itself. So it either needs to represent F in addition to N, or just F(N). Since F is computable and therefore has a finite program, you can just include the whole thing.
It is not at all evident that the length of the proof grows linearly or even polynomially with the length of the program A. This depends on the theory T, it might have a very inefficient way of denoting proofs.
Perhaps it would be easier to switch the roles of N and F(N), so you get
2) The formal theory T can prove the following statement in F(N) symbols or less: “For any program B, if the formal theory T can prove that A(B)=B(A) in N symbols or less, then A(B)=C”.
I am not sure if the corresponding variant of the bounded Löb's theorem holds, though.
the formal theory T can prove the following statement in 2*N symbols or less: "..."
The formal theory will need some additional symbols to tie everything together, so the total proof would need 2*N+K symbols, where hopefully K doesn't depend on N. This is ignoring point 2 above.
Twan, thanks for the detailed comments!
Program A needs F(N), not on N itself. So it either needs to represent F in addition to N, or just F(N). Since F is computable and therefore has a finite program, you can just include the whole thing.
Yes, the intended interpretation is that A represents F too, as do all statements that mention F. That's why in the bounded Lob's theorem the function L is stated to be computable.
...It is not at all evident that the length of the proof grows linearly or even polynomially with the length of the program A. This depends
I'm writing up some math results developed on LW as a paper with the tentative title "Self-referential decision algorithms". Something interesting came up while I was cleaning up the Loebian cooperation result. Namely, how do we say precisely that Loebian cooperation is stable under minor syntactic changes? After all, if we define a "minor change" to program A as a change that preserves A's behavior against any program B, then quining cooperation is just as stable under such "minor changes" by definition. Digging down this rabbit hole, I seem to have found a nice new reformulation of the whole thing.
I will post some sections of my current draft in the comments to this post. Eventually this material is meant to become an academic paper (hopefully), so any comments on math mistakes, notation or tone would be much appreciated! And yeah, I have no clue about academic writing, so you're welcome to tell me that too.