Algorithms and structural complexity theory Many important results in computational complexity theory, and in particular "structural" complexity theory, have the interesting property that they can be understood as fundamentally following (as I see it...) from algorithmic results giving an efficient algorithm or communication protocol for some problem. These include the following:


IP = PSPACE follows from a space-efficient recursive algorithm simulating interactive protocols, and an efficient interactive protocol for evaluating totally quantified boolean formulae. In fact any complexity class equality A=B can be seen as following from two efficient algorithms (an algorithm for problems in A which is efficient with respect to B, and vice versa).

Proving NP-completeness of some problem is just finding an efficient algorithm to reduce an NP-complete problem to it.

The (arguably!) crucial ingredient in the Time Hierarchy Theorem is an efficient universal simulation of Turing machines.

The recent result of Ryan Williams that ACC $\not \supset$ NEXP is based on an efficient algorithm to solve circuit satisfiability for ACC circuits.

The PCP Theorem is that efficient gap amplification is possible for constraint satisfaction problems.

etc., etc.


My question (which is possibly hopelessly vague!) is as follows: Are there any important results in structural complexity theory (as distinct from "meta-results" like the relativisation barrier) which are not known to have a natural interpretation in terms of efficient algorithms (or communication protocols)?
For many lower bounds in algebraic complexity, I do not know of a natural interpretation in terms of efficient algorithms. For example:


the partial derivatives technique of Nisan and Wigderson
the rank-of-Hessian technique of Mignon and Ressayre (giving the currently best known lower bound on permanent versus determinant)
the degree bound of Strassen (and Baur-Strassen)
the connected components technique of Ben-Or.


In all the above results, they really seem to be using a property of the functions involved, where that property itself seems unrelated to the existence of any particular algorithm (let alone an effective one). 

For non-algebraic results, here are a couple of thoughts:


The standard counting argument for the $n \log n$ sorting lower bound does not appear to have an interpretation in terms of efficient algorithms. However, there is an adversarial version of this lower bound [1], in which there is an algorithm which, given any decision tree that uses too few comparisons, efficiently constructs a list that the decision tree sorts incorrectly. But the adversarial version, while not difficult, is significantly more difficult than the counting proof. (Note that this is quite a bit stronger than what one gets by applying the adversary lower bound technique, e.g. as in these notes, since in [1] the adversary itself is efficient.)
I think I've changed my mind about PARITY not in $AC^0$ (even the original proof, let alone the Razborov-Smolensky proof, as pointed out by @RobinKothari). Although the Switching Lemma can be viewed as a randomized (or deterministic) algorithm that lets you swap two rows of a circuit without a big blow-up in size, I think this really has a different flavor than many results in complexity, and specifically the ones you cite. For example, Williams's proof that $ACC \neq NEXP$ is based crucially on the existence of a good algorithm for a particular problem. In contrast, if one could prove something like the Switching Lemma nonconstructively, it would be just as good for proving PARITY not in $AC^0$.


Because of these last two examples - especially sorting, where the standard proof is nonconstructive - it seems to me that the question may not just be about natural interpretations in terms of efficient algorithms, but also somehow about the constructiveness / effectiveness of the proofs of various complexity results (depending on what the OP had in mind). That is, the standard sorting lower bound is not constructive or algorithmic, but there is a constructive, algorithmic proof of the same result.

[1] Atallah, M. J. and Kosaraju, S. R. An adversary-based lower bound for sorting. Inform. Proc. Lett. 13(2):55-57, 1981.