I think the proof would be about g(n) symbols long, which is basically linear in n. Since R finds a proof shorter than g(n), exhibiting that proof yields a slightly longer proof that R stops early (because R either finds the exhibited proof, or stops even earlier). Then it’s easy to deduce that T+¬S is inconsistent, which can be converted into a proof of S from T.
I think the proof would be about g(n) symbols long, which is basically linear in n. Since R finds a proof shorter than g(n), exhibiting that proof yields a slightly longer proof that R stops early (because R either finds the exhibited proof, or stops even earlier). Then it’s easy to deduce that T+¬S is inconsistent, which can be converted into a proof of S from T.