  For a one-dimensional spin chain with random local interactions, we prove
that many-body localization follows from a physically reasonable assumption
that limits the amount of level attraction in the system. The construction uses
a sequence of local unitary transformations to diagonalize the Hamiltonian and
connect the exact many-body eigenfunctions to the original basis vectors.
