Prove2Me

Brillouin theorem: stationarity of a Slater determinant ⇔ no single excitations (Eqs. (62), (63))

Proved
KochHF.brillouin_theorem

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

hartree-fockmathematical-physicssecond-quantization

Let H^\hat H be a hermitian operator on Fock space, α1,…,αN∈CK\alpha_1,\dots,\alpha_N\in\mathbb C^K orthonormal orbitals and ∣Φ⟩=cαN†⋯cα1†∣0⟩|\Phi\rangle=c^\dagger_{\alpha_N}\cdots c^\dagger_{\alpha_1}|0\rangle. For a hermitian K×KK\times K matrix MM put M^=∑αβMαβcα†cβ\hat M=\sum_{\alpha\beta}M_{\alpha\beta}c^\dagger_\alpha c_\beta and EM(λ)=⟨Φ∣eiλM^H^e−iλM^∣Φ⟩E_M(\lambda)=\langle\Phi|e^{i\lambda\hat M}\hat He^{-i\lambda\hat M}|\Phi\rangle. Then the following are equivalent:

  1. (Stationarity) for every hermitian MM, EME_M has derivative 00 at λ=0\lambda=0;
  2. (Brillouin condition) for every occupied orbital φo∈span⁡{α1,…,αN}\varphi_o\in\operatorname{span}\{\alpha_1,\dots,\alpha_N\} and every virtual orbital φv⊥α1,…,αN\varphi_v\perp\alpha_1,\dots,\alpha_N,
⟨Φ∣ cφo†cφv H^ ∣Φ⟩=0.\langle\Phi|\,c^\dagger_{\varphi_o}c_{\varphi_v}\,\hat H\,|\Phi\rangle=0 .

In words: a Slater determinant is a stationary point of the energy under all one-body unitary variations exactly when the Hamiltonian has no matrix elements between it and its singly excited determinants. This is the variational characterization of Hartree-Fock determinants on which the self-consistent field method rests.

Formalization Note The source states (63) with orthonormal reference orbitals m≤Nm\le N occupied and n>Nn>N virtual; the formal statement quantifies over all occupied and all virtual orbitals, which is the basis-independent form of the same condition.

Preamble
import Mathlib
import Definitions.Def_KochHF_FockSpace

open Matrix
Formal statement
namespace KochHF

theorem brillouin_theorem {K N : ℕ} (H : FockOp K) (hH : H.IsHermitian)
    (α : Fin N → Fin K → ℂ) (hα : ∀ i j, orbInner (α i) (α j) = if i = j then 1 else 0) :
    (∀ M : Matrix (Fin K) (Fin K) ℂ, M.IsHermitian →
      HasDerivAt
        (fun t : ℝ => matEl (slater α)
          (NormedSpace.exp ((Complex.I * t) • oneBodyOp M) * H *
            NormedSpace.exp ((-(Complex.I * t)) • oneBodyOp M)) (slater α))
        0 0) ↔
    (∀ φo φv : Fin K → ℂ, φo ∈ Submodule.span ℂ (Set.range α) →
      (∀ i, orbInner (α i) φv = 0) →
      matEl (slater α) (cdagOrb φo * cannOrb φv * H) (slater α) = 0) := 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.16–2.17, Eqs. (55), (61)–(63) ("the Brillouin theorem").
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∈NK\in\mathbb N is the number of orthonormal reference orbitals ϕ0,…,ϕK−1\phi_0,\dots,\phi_{K-1}; an orbital is a coefficient vector φ∈CK\varphi\in\mathbb C^K and ⟨φ∣χ⟩=∑μφμ‾χμ\langle\varphi|\chi\rangle=\sum_\mu\overline{\varphi_\mu}\chi_\mu. Fock space is C2K\mathbb C^{2^K} with orthonormal basis ∣S⟩|S\rangle, S⊆{0,…,K−1}S\subseteq\{0,\dots,K-1\}; ci†∣S⟩=(−1)#{j∈S: j>i}∣S∪{i}⟩c^\dagger_i|S\rangle=(-1)^{\#\{j\in S:\,j>i\}}|S\cup\{i\}\rangle for i∉Si\notin S and 00 for i∈Si\in S; ci=(ci†)†c_i=(c_i^\dagger)^\dagger (conjugate transpose); cφ†=∑μφμcμ†c^\dagger_\varphi=\sum_\mu\varphi_\mu c^\dagger_\mu, cφ=∑μφμ‾cμc_\varphi=\sum_\mu\overline{\varphi_\mu}c_\mu; ∣0⟩=∣∅⟩|0\rangle=|\emptyset\rangle; for orbitals α0,…,αN−1\alpha_0,\dots,\alpha_{N-1} the vector ∣Φα⟩=cαN−1†⋯cα0†∣0⟩|\Phi_\alpha\rangle=c^\dagger_{\alpha_{N-1}}\cdots c^\dagger_{\alpha_0}|0\rangle (for N=0N=0 this is ∣0⟩|0\rangle). For all K,NK,N, every Fock-space operator HH that is hermitian (H†=HH^\dagger=H), and every orthonormal family α0,…,αN−1∈CK\alpha_0,\dots,\alpha_{N-1}\in\mathbb C^K (hypothesis ⟨αi∣αj⟩=δij\langle\alpha_i|\alpha_j\rangle=\delta_{ij}), the following two statements are equivalent:

(A) For every hermitian K×KK\times K complex matrix MM, the function t↦⟨Φα∣exp⁡(itM^) H exp⁡(−itM^)∣Φα⟩t\mapsto\langle\Phi_\alpha|\exp(it\hat M)\,H\,\exp(-it\hat M)|\Phi_\alpha\rangle from R\mathbb R to C\mathbb C has derivative 00 at t=0t=0 (this includes the assertion that it is differentiable there), where M^=∑a,bMabca†cb\hat M=\sum_{a,b}M_{ab}c^\dagger_ac_b.

(B) For all φo,φv∈CK\varphi_o,\varphi_v\in\mathbb C^K such that φo\varphi_o lies in the complex linear span of {α0,…,αN−1}\{\alpha_0,\dots,\alpha_{N-1}\} and ⟨αi∣φv⟩=0\langle\alpha_i|\varphi_v\rangle=0 for every ii, one has

⟨Φα∣ cφo† cφv H ∣Φα⟩=0.\langle\Phi_\alpha|\,c^\dagger_{\varphi_o}\,c_{\varphi_v}\,H\,|\Phi_\alpha\rangle=0 .

Edge cases: for N=0N=0, ∣Φ⟩=∣0⟩|\Phi\rangle=|0\rangle, the span is {0}\{0\} and (B) holds trivially; for N=KN=K the only virtual orbital is 00 and (B) holds trivially. In both cases the theorem asserts that (A) holds as well.

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