Energy of a Slater determinant (Hartree-Fock energy, Sec. 3.2)

Proved

KochHF.hartree_fock_energy

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

hartree-fockmathematical-physicssecond-quantization

With $\hat H$ , $T$ , $U$ as in the definition file and $U_{nn',mm'}=U_{n'n,m'm}$ , the energy of the determinant $|S\rangle$ of occupied reference orbitals $S$ is

\langle S|\hat H|S\rangle=\sum_{m\in S}\Bigl(T_{mm}+\sum_{m'\in S,\,m'<m}\Delta_{mm'}\Bigr)=\sum_{m\in S}\Bigl(T_{mm}+\tfrac12\sum_{m'\in S}\Delta_{mm'}\Bigr),

where $\Delta_{mm'}=U_{mm',mm'}-U_{mm',m'm}$ .

This is the Hartree-Fock total energy expressed through direct and exchange integrals of the occupied orbitals.

Preamble

import Mathlib
import Definitions.Def_KochHF_FockSpace
import Definitions.Def_KochHF_Hamiltonian

open Matrix

Formal statement

namespace KochHF

theorem hartree_fock_energy {K : ℕ} (T : Matrix (Fin K) (Fin K) ℂ)
    (U : Fin K → Fin K → Fin K → Fin K → ℂ) (hU : ∀ n n' m m', U n n' m m' = U n' n m' m)
    (S : Finset (Fin K)) :
    detEnergy T U S = ∑ m ∈ S, (T m m + ∑ m' ∈ S.filter (· < m), hfDelta U m m') ∧
    detEnergy T U S = ∑ m ∈ S, (T m m + (1 / 2 : ℂ) * ∑ m' ∈ S, hfDelta U m m') := by sorry

end KochHF

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, p. 2.18, Eq. (65) and the displayed Hartree-Fock energy following it; symmetry from Sec. 2.3.2, p. 2.11.

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.

Throughout, $K\in\mathbb N$ is the number of orthonormal reference orbitals $\phi_0,\dots,\phi_{K-1}$ ; an orbital is a coefficient vector $\varphi\in\mathbb C^K$ and $\langle\varphi|\chi\rangle=\sum_\mu\overline{\varphi_\mu}\chi_\mu$ . Fock space is $\mathbb C^{2^K}$ with orthonormal basis $|S\rangle$ , $S\subseteq\{0,\dots,K-1\}$ ; $c^\dagger_i|S\rangle=(-1)^{\#\{j\in S:\,j>i\}}|S\cup\{i\}\rangle$ for $i\notin S$ and $0$ for $i\in S$ ; $c_i=(c_i^\dagger)^\dagger$ (conjugate transpose); $c^\dagger_\varphi=\sum_\mu\varphi_\mu c^\dagger_\mu$ , $c_\varphi=\sum_\mu\overline{\varphi_\mu}c_\mu$ ; $|0\rangle=|\emptyset\rangle$ ; for orbitals $\alpha_0,\dots,\alpha_{N-1}$ the vector $|\Phi_\alpha\rangle=c^\dagger_{\alpha_{N-1}}\cdots c^\dagger_{\alpha_0}|0\rangle$ (for $N=0$ this is $|0\rangle$ ). For all $K$ , every complex $K\times K$ matrix $T$ , every complex 4-index array $U$ with $U_{nn'mm'}=U_{n'nm'm}$ for all indices, and every $S\subseteq\{0,\dots,K-1\}$ , writing $E(S)=\langle S|\hat H(T,U)|S\rangle$ and $\Delta_{mm'}=U_{mm'mm'}-U_{mm'm'm}$ , both of the following hold:

$E(S)=\sum_{m\in S}\bigl(T_{mm}+\sum_{m'\in S,\ m'<m}\Delta_{mm'}\bigr)$ ;
$E(S)=\sum_{m\in S}\bigl(T_{mm}+\tfrac12\sum_{m'\in S}\Delta_{mm'}\bigr)$ .

For $S=\emptyset$ both sides are $0$ .

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