Is there a formal theorem making this precise?

I'm not familiar with the formal definition of Kolmogorov complexity, nor its related theorems, but informally, it appears to be about the length of the specifying program, not the time it takes to run.

Given that we have a finite domain, and 1:1 functions, we should be able to specify f^-1 with some constant overhead and embedding f.

Something along the lines of:

  //embed the definition of f.
  f^-1(x) = for a in Domain:
    if f(a) = x
      return a

Formalizing this would involve specifying what description language you are using and how you encode functions.