The theorem was first proved in 1975 by Shmuel Elitzur in lattice field theory,[1] although the same result is expected to hold in the continuum limit.
This is a consequence of Noether's second theorem which states that each local symmetry degree of freedom corresponds to a relation among the Euler–Lagrange equations, making the system underdetermined.
Underdeterminacy requires gauge fixing of the non-propagating degrees of freedom so that the equations of motion admit a unique solution.
Such non-invariant local operators always have vanishing vacuum expectation values for finite size systems, prohibiting spontaneous symmetry breaking.
This occurs because over large timescales, finite systems always transition between all possible ground states, averaging away the expectation value of the operator.
[7] This is also an explanation for why gauge symmetries are mere redundancies in lattice field theories, where the equations of motion need not define a well-posed problem as they do not need to be solved.
Instead, Elitzur's theorem shows that any observable that is not invariant under the symmetry has a vanishing expectation value, making it unobservable and therefore redundant.
It is therefore in principle plausible that there may exist exotic continuum theories for which gauge symmetries can be spontaneously broken, although such a scenario remains unlikely due to the absence of any known examples.
The generalized Elitzur's theorem then provides bounds on the vacuum expectation values of operators that are non-invariant under such d-dimensional symmetries.