Single-excitation matrix elements of $\hat H$ are Fock-matrix entries (Eq. (64))

Proved

KochHF.fock_matrix_single_excitation

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

hartree-fockmathematical-physicssecond-quantization

Let $\hat H=\sum_{n,m}c^\dagger_nT_{nm}c_m+\sum_{n>n',m>m'}c^\dagger_nc^\dagger_{n'}(U_{nn',mm'}-U_{nn',m'm})c_{m'}c_m$ with two-body matrix elements satisfying the exchange symmetry $U_{nn',mm'}=U_{n'n,m'm}$ (Sec. 2.3.2). Let $|S\rangle$ be the determinant of the occupied reference orbitals $S$ . Then for every virtual $n\notin S$ and occupied $m\in S$ ,

\langle S|\,c^\dagger_m c_n\,\hat H\,|S\rangle=F_{nm}=T_{nm}+\sum_{m'\in S}\bigl(U_{nm',mm'}-U_{nm',m'm}\bigr).

So for this Hamiltonian the Brillouin condition says exactly that the occupied–virtual block of the Fock matrix vanishes; this is why Hartree-Fock reduces to a self-consistent one-body problem.

Preamble

import Mathlib
import Definitions.Def_KochHF_FockSpace
import Definitions.Def_KochHF_Hamiltonian

open Matrix

Formal statement

namespace KochHF

theorem fock_matrix_single_excitation {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)) (n m : Fin K) (hn : n ∉ S) (hm : m ∈ S) :
    matEl (basisState S) (cdag m * cann n * hamiltonian T U) (basisState S) =
      fockMatrix T U S n 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, pp. 2.17–2.18, Hamiltonian preceding Eq. (64) and Eq. (64); symmetry

M_{nn',mm'}=M_{n'n,m'm}

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$ satisfying $U_{nn'mm'}=U_{n'nm'm}$ for all indices, every $S\subseteq\{0,\dots,K-1\}$ and all $n\notin S$ , $m\in S$ :

\langle S|\,c^\dagger_m\,c_n\,\hat H(T,U)\,|S\rangle=T_{nm}+\sum_{m'\in S}\bigl(U_{nm'mm'}-U_{nm'm'm}\bigr),

where $\hat H(T,U)=\sum_{n,m}T_{nm}c^\dagger_nc_m+\sum_{n'<n,\ m'<m}(U_{nn'mm'}-U_{nn'm'm})\,c^\dagger_nc^\dagger_{n'}c_{m'}c_m$ and $c^\dagger_m,c_n$ are reference-orbital operators. No hermiticity of $T$ or $U$ is assumed.

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

Single-excitation matrix elements of H^\hat HH^ are Fock-matrix entries (Eq. (64))

Single-excitation matrix elements of $\hat H$ are Fock-matrix entries (Eq. (64))