Motivation

The Hartree-Fock method approximates the ground state of an interacting many-electron system by the best single Slater determinant. It is the starting point of essentially all of quantum chemistry and of mean-field theories in condensed-matter physics: post-Hartree-Fock methods (configuration interaction, coupled cluster, perturbation theory) expand around it, and its orbital energies are the standard first estimate of ionization and excitation energies. E. Koch's lecture notes Mean-Field Theory: Hartree-Fock and BCS (Jülich Autumn School on Correlated Electrons, 2016) derive the method entirely within second quantization: Slater determinants are products of creation operators acting on a vacuum, variations are generated by one-body unitaries $e^{i\lambda\hat M}$, and the stationarity condition becomes an algebraic statement about matrix elements. The central result of the Hartree-Fock section is the Brillouin theorem: a Slater determinant is stationary exactly when the Hamiltonian does not couple it to its single excitations.

Timeline of the ideas involved: Hartree introduces the self-consistent field (1928); Fock and Slater add exchange through antisymmetrized wave functions (1930); Koopmans relates orbital energies to ionization energies (1934); Brillouin formulates the single-excitation condition (1934); Thouless gives the representation of Slater determinants by exponentials of one-body operators (1960).

Setting

Fix $K$ orthonormal reference orbitals $\phi_0,\dots,\phi_{K-1}$; an orbital is a coefficient vector $\varphi\in\mathbb C^K$ with $\langle\varphi|\chi\rangle=\sum_\mu\overline{\varphi_\mu}\chi_\mu$. The Fock space has orthonormal basis $|S\rangle$, $S\subseteq\{0,\dots,K-1\}$ (the set of occupied orbitals). The creation operator $c^\dagger_i$ maps $|S\rangle$ to $(-1)^{\#\{j\in S:\,j>i\}}|S\cup\{i\}\rangle$ if $i\notin S$ and to $0$ otherwise; the annihilation operator $c_i$ is its adjoint, and for a general orbital $c^\dagger_\varphi=\sum_\mu\varphi_\mu c^\dagger_\mu$. The vacuum is $|0\rangle=|\emptyset\rangle$.

The Slater determinant of orbitals $\alpha_1,\dots,\alpha_N$ is $|\Phi\rangle=c^\dagger_{\alpha_N}\cdots c^\dagger_{\alpha_1}|0\rangle$. A one-body operator with matrix $M$ is $\hat M=\sum_{\alpha\beta}M_{\alpha\beta}c^\dagger_\alpha c_\beta$. For a hermitian $M$ the operators $e^{i\lambda\hat M}$ map Slater determinants to Slater determinants, and the energy functional along such a variation is

$$E_M(\lambda)=\langle\Phi|e^{i\lambda\hat M}\,\hat H\,e^{-i\lambda\hat M}|\Phi\rangle .$$

For the concrete Hamiltonian of Sec. 3.2,

$$\hat H=\sum_{n,m}c^\dagger_nT_{nm}c_m+\sum_{n>n',\,m>m'}c^\dagger_nc^\dagger_{n'}\bigl(U_{nn',mm'}-U_{nn',m'm}\bigr)c_{m'}c_m,$$

the Fock matrix of the determinant with occupied reference orbitals $S$ is $F_{nm}=T_{nm}+\sum_{m'\in S}(U_{nm',mm'}-U_{nm',m'm})$, with diagonal entries the orbital energies $\varepsilon_m$.

Formalization targets

Goal: the Brillouin theorem (Eqs. (62)–(63))

For a hermitian $\hat H$ and orthonormal $\alpha_1,\dots,\alpha_N$,

$$\Bigl(\forall M=M^\dagger:\ E_M'(0)=0\Bigr)\iff\Bigl(\forall\,\varphi_o\in\operatorname{span}\{\alpha_n\},\ \varphi_v\perp\{\alpha_n\}:\ \langle\Phi|c^\dagger_{\varphi_o}c_{\varphi_v}\hat H|\Phi\rangle=0\Bigr).$$

It asserts no specific Hamiltonian, no particle number and no basis choice; it is the basis-independent form of the source's condition (63).

Milestones

The milestone list follows the source's own steps: the anticommutation relations (15); the overlap formula (7)/(46); the action of $c_\varphi$, $c^\dagger_\varphi$ on a determinant (42); the one-body density matrix (43) and Wick's theorem (45); the transformation of vacuum and creators under $e^{i\lambda\hat M}$ (57), (59); the first-order variation (61)–(62). For the two-body Hamiltonian it adds the Fock-matrix form of the Brillouin condition (64), the Hartree-Fock energy, Koopmans' theorem (66) and the electron-hole excitation energy (67).

Significance

The Brillouin theorem turns the nonlinear variational problem over all Slater determinants into a condition on finitely many matrix elements; for a two-body Hamiltonian it says that the occupied–virtual block of the Fock matrix vanishes, which is the self-consistency condition solved by every Hartree-Fock code. Koopmans' theorem and the particle-hole formula give the physical interpretation of the orbital energies.

All results are classical and proved in the source and in standard textbooks. What this mission adds is a machine-checked account of second quantization on a finite orbital basis: the anticommutation relations, determinant overlaps and Wick's theorem for Slater determinants are reusable for any later formalization of configuration interaction, coupled cluster or BCS theory.

Difficulty

The source's arguments are short manipulations of operator identities, but each hides bookkeeping that is easy to get wrong: fermionic signs when operators are reordered, the identification of Slater determinants with ordered products of creators, and the Laplace expansion behind Wick's theorem. The variational step requires differentiating a matrix exponential on Fock space and identifying the derivative with a commutator. The direction from the Brillouin condition back to stationarity needs the hermiticity of $\hat H$ and a decomposition of an arbitrary hermitian $M$ into occupied–occupied, virtual–virtual and occupied–virtual blocks; the first two blocks act on $|\Phi\rangle$ only by a scalar. The Fock-matrix milestones additionally need the exchange symmetry $U_{nn',mm'}=U_{n'n,m'm}$ of two-body matrix elements stated in Sec. 2.3.2; without it the stated formulas fail.

Formalization scope

Fock space over $K$ orbitals is represented concretely: vectors are functions on Finset (Fin K) and operators are complex matrices indexed by Finset (Fin K). Creators carry the sign $(-1)^{\#\{j\in S:\,j>i\}}$, so ordered products of creators of increasing orbitals give $+|S\rangle$. All quantities are complex; the exponential is NormedSpace.exp; stationarity is HasDerivAt … 0 0 for a function $\mathbb R\to\mathbb C$. Orthonormality of the occupied orbitals is an explicit hypothesis wherever the source assumes it. The source works with a possibly infinite orbital basis; here the basis is finite, as in the variational setting of its Sec. 3.

The equivalence in the goal cannot be satisfied vacuously: hermiticity of $\hat H$ and orthonormality of the orbitals are both satisfiable, and both sides quantify over all admissible $M$, respectively all occupied and virtual orbitals.

Two printed formulas are not taken verbatim: Eq. (60) lacks the minus sign in the exponent and is omitted, and Eq. (61) prints the first-order commutator in the opposite order; the milestone records the correct derivative $i\langle\Phi|[\hat M,\hat H]|\Phi\rangle$, which leaves (62) unchanged.

Contributions welcome: a general API for products of creation and annihilation operators in this model (sign lemmas, normal ordering), which all milestones share.

Selected references

• E. Koch, Mean-Field Theory: Hartree-Fock and BCS, in E. Pavarini, E. Koch, J. van den Brink, G. Sawatzky (eds.), Quantum Materials: Experiments and Theory, Modeling and Simulation Vol. 6, Forschungszentrum Jülich, 2016. http://www.cond-mat.de/events/correl16
• A. Szabo and N. S. Ostlund, Modern Quantum Chemistry: Introduction to Advanced Electronic Structure Theory, Dover, 1996.
• T. Koopmans, Über die Zuordnung von Wellenfunktionen und Eigenwerten zu den einzelnen Elektronen eines Atoms, Physica 1 (1934) 104–113.