maybe we don't need that to achieve at least some provable polynomial separation between evaluating a function, and reversing it. Even a problem with $\Omega(n^7)$ could suffice to build somewhat practical cryptography: $c⋅(2128)17≈c⋅319557$ bits (for some constant $c$) would be required to obtain the same security level as a 128 bit key.
Some people have tried thinking about this. The relevant name is "fine-grained cryptography". You can show things like what you allude to --- some polynomial "gap" in the complexity of honest parties vs adversarial ones. One of Ralph Merkle's early cryptosystems (the "Merkle Puzzles") was actually of this form. It was arguably the earliest publicly-known (GCHQ had something earlier I believe) public-key cryptosystem, but only in the aformentioned "fine-grained" sense. Here, you still need to make some hardness assumption --- in particular you need a random oracle. But you get public-key cryptography from a random oracle, although only with a polynomial computation gap.
If you're ok with even weaker crypto, you can remove additional assumptions to get "fully provable" results.
In particular, you can get are things like "There exists a circuit, computable in $AC^0$, whose inverse is not" (so an OWF for $AC^0$). See the introduction of this paper for references.
For example, for comparison based sorting, we know you need $\Omega(n \log n)$ comparisons.
This is a good example, as it's an example of lower bounds we know how to prove. In general, we only know  how to prove lower bounds on restricted models of computation. Examples include:
- The decision tree complexity of a problem (the $\Omega(n \log n)$ lower bound on comparisons for sorting is of this form)
- The communication complexity of a problem (I've seen this show up in a time/space tradeoff paper in cryptography before)
- Lower bounds in the generic group model
There are other lower bounds of course that are applicable within cryptography (I have work in progress which uses some sphere packing lower bounds, for example), but they are much more specialized.
 One can prove lower bounds on specific problems which are conjectured to be hard in the Turing machine model of computation, but they are very weak. In particular, I think our best lower bounds on 3-SAT are only linear (with a constant of like $4$ or something).