How does this proof show that sequences of $O(1)$ polynomially bounded Kolmogorov complexity are NOT the polynomial computable ones? I'm trying to understand a proof from the paper: Balcázar, José L.; Gavaldà, Ricard; Hermo, Montserrat: Compressiblity of infinite binary sequences, Published in: Complexity, Logic, and Recursion Theory, A. Sorbi, ed., Marcel Dekker 1997, ISBN 0-8247-0026-0, 75-91.

Theorem 19 For every recursive time bound f , there is an infinite sequence that is in $C4[O(1), poly]$ but not $DTIME(f (n))$-computable. (The sequence is automatically in $C5[O(1), poly]$ and in $CK[O(1), poly]$.)
Proof: The main idea is to build a tally set $T\subseteq\{0\}^*$ with the following properties:

$\chi^T$ is not $DTIME(f (n))$-computable, where $\chi^T$ is the characteristic sequence of $T$ over $\{0\}^*$

$T \in\ DTIME(g(n))$, for some nondecreasing time-constructible time bound $g$ such
that $g(n) \gt f (n)$.

strings in $T$ are very far one from another; more precisely, $T$ contains only strings of
the form $0^{s(m)}$
, where $s$ is defined inductively by:
$s(1) = 1;$      $s(m + 1) = g(s(m))$
[...]



(the proof proceeds by using the third property to show that it's easy/polynomial to create $\chi^{T \leq n}$ up to an uncertainty in exactly one hard bit, and so it is possible to consider two machines, one answering $1$ and an other answering $0$ for it, fulfilling the requirement of $\chi^T$ being in $C4[O(1), poly]$ )
This Theorem is claiming to build a tally set that does the job, and I understand how the proof proceeds, once it is taken granted that the set with the specified properties exists, but I don't see its existence proven.
How do we know that such a tally set exists for every recursive $f(n)$ that is not $\mathrm{DTIME}(f(n))$ computable as specified in property (1)?
And why do we have to guarantee in property (2) that the $g(n)$ bound is greater or equal to $f(n)$?
Am I missing something basic about tally sets, or sets vs characteristic sequences in general, or some trivial hierarchy theorem?
Wow, that was sooooo long ago. Something like the early nineties...

The point is, for that T, at the time of writing, the construction proper was assumed to be well-established in the background knowledge of any potential reader. Thus, we did not give details. Essentially, what you do is a Cantor-like proof as in the non-numerability of the reals: for each i, run the i-th DTIME(f) machine on a string of s(i) zeros, and add that string to T if and only if the simulated machine rejects it. (Colloquially that string was often called "the cookie".) Then g is to be any time-constructible function that allows for this process to be completed - for this we will need it considerably larger than f. There is a slight circularity in that the process depends on s, which depends on g, which is defined as sufficient time to run the process. But it is easy to upper bound this time and select a sensible g.

Hope this helps! (And hope this works. It is my first time writing anything into stackexchange.)