Prove2Me

Wick's theorem for Slater determinants: pp-body density matrices are determinants (Eq. (45))

Proved
KochHF.slater_wick

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

hartree-fockmathematical-physicssecond-quantization

Let α1,…,αN∈CK\alpha_1,\dots,\alpha_N\in\mathbb C^K be orthonormal and ∣Φ⟩=cαN†⋯cα1†∣0⟩|\Phi\rangle=c^\dagger_{\alpha_N}\cdots c^\dagger_{\alpha_1}|0\rangle, with one-body density matrix Γnm(1)=⟨Φ∣cn†cm∣Φ⟩\Gamma^{(1)}_{nm}=\langle\Phi|c^\dagger_nc_m|\Phi\rangle. For every p≥0p\ge0 and reference indices n1,…,npn_1,\dots,n_p, m1,…,mpm_1,\dots,m_p,

⟨Φ∣cnp†⋯cn1† cm1⋯cmp∣Φ⟩=det⁡(Γn1m1(1)⋯Γn1mp(1)⋮⋱⋮Γnpm1(1)⋯Γnpmp(1)).\langle\Phi|c^\dagger_{n_p}\cdots c^\dagger_{n_1}\,c_{m_1}\cdots c_{m_p}|\Phi\rangle=\det\begin{pmatrix}\Gamma^{(1)}_{n_1m_1}&\cdots&\Gamma^{(1)}_{n_1m_p}\\ \vdots&\ddots&\vdots\\ \Gamma^{(1)}_{n_pm_1}&\cdots&\Gamma^{(1)}_{n_pm_p}\end{pmatrix}.

All higher-order density matrices of a Slater determinant are thus determined by its one-body density matrix; the case p=2p=2 is Eq. (44).

Preamble
import Mathlib
import Definitions.Def_KochHF_FockSpace

open Matrix
Formal statement
namespace KochHF

theorem slater_wick {K N p : ℕ} (α : Fin N → Fin K → ℂ)
    (hα : ∀ i j, orbInner (α i) (α j) = if i = j then 1 else 0) (n m : Fin p → Fin K) :
    matEl (slater α)
        ((List.ofFn fun i => cdag (n i)).reverse.prod * (List.ofFn fun i => cann (m i)).prod)
        (slater α) =
      (Matrix.of fun i j => matEl (slater α) (cdag (n i) * cann (m j)) (slater α)).det := 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. 2.4, pp. 2.12–2.13, Eqs. (44), (45).
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,N,pK,N,p, 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}) and all index tuples n0,…,np−1n_0,\dots,n_{p-1} and m0,…,mp−1m_0,\dots,m_{p-1} in {0,…,K−1}\{0,\dots,K-1\} (repetitions allowed):

⟨Φα∣ cnp−1†⋯cn0†  cm0⋯cmp−1 ∣Φα⟩=det⁡(⟨Φα∣cni†cmj∣Φα⟩)i,j=0p−1.\langle\Phi_\alpha|\,c^\dagger_{n_{p-1}}\cdots c^\dagger_{n_0}\;c_{m_0}\cdots c_{m_{p-1}}\,|\Phi_\alpha\rangle=\det\Bigl(\langle\Phi_\alpha|c^\dagger_{n_i}c_{m_j}|\Phi_\alpha\rangle\Bigr)_{i,j=0}^{p-1}.

For p=0p=0 the operator is the identity and both sides equal 11 (using ⟨Φα∣Φα⟩=1\langle\Phi_\alpha|\Phi_\alpha\rangle=1, which is not assumed but must follow).

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