Hartree-Fock Hamiltonian, Fock matrix and orbital energies

Definition

KochHF_Hamiltonian

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

hartree-fockmathematical-physicssecond-quantization

Let $T$ be a complex $K\times K$ matrix (one-body matrix elements) and $U_{nn',mm'}$ a complex 4-index array (two-body matrix elements). Following Sec. 3.2 the Hamiltonian with one- and two-body terms is

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

For a set $S$ of occupied reference orbitals (the determinant $|S\rangle$ ):

$\Delta_{mm'}=U_{mm',mm'}-U_{mm',m'm}$ (Eq. (65));
the Fock matrix (Eq. (64)) $F_{nm}=T_{nm}+\sum_{m'\in S}\bigl(U_{nm',mm'}-U_{nm',m'm}\bigr)$ ;
the Hartree-Fock orbital energy (Eq. (65)) $\varepsilon_m=F_{mm}=T_{mm}+\sum_{m'\in S}\Delta_{mm'}$ ;
the determinant energy $E(S)=\langle S|\hat H|S\rangle$ .

These definitions are used in the milestones on the Fock matrix, the Hartree-Fock energy, Koopmans' theorem and electron-hole excitation energies.

Formalization Note The occupied orbitals are an arbitrary subset $S$ of the reference orbitals rather than the first $N$ of them; $\varepsilon_m$ is defined as the diagonal entry $F_{mm}$ , which is the source's Eq. (65) and coincides with the Fock eigenvalue when $F$ is diagonal (self-consistency).

Definition code

import Mathlib
import Definitions.Def_KochHF_FockSpace

/-!
# The Hartree-Fock Hamiltonian, Fock matrix and orbital energies

E. Koch, *Mean-Field Theory: Hartree-Fock and BCS*, Sec. 3.2 (Hamiltonian before Eq. (64),
Eqs. (64), (65)).
-/

noncomputable section

namespace KochHF

/-- `Ĥ = Σ_{n,m} c†_n T_{nm} c_m + Σ_{n>n', m>m'} c†_n c†_{n'} (U_{nn',mm'} - U_{nn',m'm}) c_{m'} c_m`
(Sec. 3.2). -/
def hamiltonian {K : ℕ} (T : Matrix (Fin K) (Fin K) ℂ) (U : Fin K → Fin K → Fin K → Fin K → ℂ) :
    FockOp K :=
  (∑ n, ∑ m, T n m • (cdag n * cann m)) +
    ∑ n, ∑ n', ∑ m, ∑ m',
      if n' < n ∧ m' < m then
        (U n n' m m' - U n n' m' m) • (cdag n * cdag n' * cann m' * cann m)
      else 0

/-- `Δ_{mm'} = U_{mm',mm'} - U_{mm',m'm}` (Eq. (65)). -/
def hfDelta {K : ℕ} (U : Fin K → Fin K → Fin K → Fin K → ℂ) (m m' : Fin K) : ℂ :=
  U m m' m m' - U m m' m' m

/-- Fock matrix of the determinant with occupied reference orbitals `S` (Eq. (64)):
`F_{nm} = T_{nm} + Σ_{m' ∈ S} (U_{nm',mm'} - U_{nm',m'm})`. -/
def fockMatrix {K : ℕ} (T : Matrix (Fin K) (Fin K) ℂ) (U : Fin K → Fin K → Fin K → Fin K → ℂ)
    (S : Finset (Fin K)) (n m : Fin K) : ℂ :=
  T n m + ∑ m' ∈ S, (U n m' m m' - U n m' m' m)

/-- Hartree-Fock orbital energy `ε_m = F_{mm} = T_{mm} + Σ_{m' ∈ S} Δ_{mm'}` (Eq. (65)). -/
def hfOrbitalEnergy {K : ℕ} (T : Matrix (Fin K) (Fin K) ℂ)
    (U : Fin K → Fin K → Fin K → Fin K → ℂ) (S : Finset (Fin K)) (m : Fin K) : ℂ :=
  fockMatrix T U S m m

/-- Energy expectation value `⟨S|Ĥ|S⟩` of the Slater determinant `|S⟩ = Π_{m ∈ S} c†_m |0⟩`
of reference orbitals. -/
def detEnergy {K : ℕ} (T : Matrix (Fin K) (Fin K) ℂ) (U : Fin K → Fin K → Fin K → Fin K → ℂ)
    (S : Finset (Fin K)) : ℂ :=
  matEl (basisState S) (hamiltonian T U) (basisState S)

end KochHF

end

Source

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, ISBN 978-3-95806-159-0, http://www.cond-mat.de/events/correl16, Sec. 3.2, pp. 2.17–2.18: Hamiltonian preceding Eq. (64), Eqs. (64), (65).

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — NON-BLIND: same agent that drafted the statements

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statement, with full knowledge of the source text and of the intended meaning. It is not a blind audit and must not be mistaken for independent testimony; reviewers should compare the Lean code against the source themselves.

Parameters: $K\in\mathbb N$ , an arbitrary complex $K\times K$ matrix $T$ , and an arbitrary function $U$ of four indices in $\{0,\dots,K-1\}$ with complex values (no symmetry or hermiticity is imposed in this file). Using the creators $c^\dagger_i$ , annihilators $c_i$ and basis states $|S\rangle$ of the Fock-space definition file:

$\hat H(T,U)=\sum_{n,m}T_{nm}\,c^\dagger_nc_m+\sum_{n,n',m,m'}[\,n'<n\text{ and }m'<m\,]\,\bigl(U_{n n' m m'}-U_{n n' m' m}\bigr)\,c^\dagger_n c^\dagger_{n'} c_{m'} c_m$ , where all four indices range over $\{0,\dots,K-1\}$ and the bracket is $1$ if the condition holds and $0$ otherwise.
$\Delta_{mm'}=U_{m m' m m'}-U_{m m' m' m}$ .
For a finite set $S\subseteq\{0,\dots,K-1\}$ : $F^S_{nm}=T_{nm}+\sum_{m'\in S}\bigl(U_{n m' m m'}-U_{n m' m' m}\bigr)$ , and $\varepsilon^S_m=F^S_{mm}$ .
$E(S)=\langle S|\hat H(T,U)|S\rangle$ , the diagonal matrix element of $\hat H$ in the basis state $|S\rangle$ .

For $S=\emptyset$ the sums over $S$ are empty, so $F^\emptyset=T$ .

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph