Prove2Me

Fock-space unitaries eiλM^e^{i\lambda\hat M} fix the vacuum and rotate creators (Eqs. (57), (59))

Proved
KochHF.one_body_unitary_transform

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

hartree-fockmathematical-physicssecond-quantization

Let MM be a hermitian K×KK\times K matrix, M^=∑αβMαβcα†cβ\hat M=\sum_{\alpha\beta}M_{\alpha\beta}c^\dagger_\alpha c_\beta and λ∈R\lambda\in\mathbb R. Then

eiλM^∣0⟩=∣0⟩andeiλM^ cγ† e−iλM^=∑αcα† (eiλM)αγe^{i\lambda\hat M}|0\rangle=|0\rangle\qquad\text{and}\qquad e^{i\lambda\hat M}\,c^\dagger_\gamma\,e^{-i\lambda\hat M}=\sum_\alpha c^\dagger_\alpha\,\bigl(e^{i\lambda M}\bigr)_{\alpha\gamma}

for every reference orbital γ\gamma.

Consequently U^(λ)=eiλM^\hat U(\lambda)=e^{i\lambda\hat M} maps Slater determinants to Slater determinants formed in the rotated orbital basis; this is the family of variations used in Hartree-Fock theory.

Preamble
import Mathlib
import Definitions.Def_KochHF_FockSpace

open Matrix
Formal statement
namespace KochHF

theorem one_body_unitary_transform {K : ℕ} (M : Matrix (Fin K) (Fin K) ℂ) (hM : M.IsHermitian)
    (t : ℝ) (γ : Fin K) :
    NormedSpace.exp ((Complex.I * t) • oneBodyOp M) *ᵥ vacuum K = vacuum K ∧
    NormedSpace.exp ((Complex.I * t) • oneBodyOp M) * cdag γ *
        NormedSpace.exp ((-(Complex.I * t)) • oneBodyOp M) =
      ∑ a, NormedSpace.exp ((Complex.I * t) • M) a γ • cdag a := 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.16, Eqs. (55)–(59).
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 KK, every K×KK\times K complex matrix MM that is hermitian (M†=MM^\dagger=M), every real tt and every reference index γ\gamma: with M^=∑a,bMabca†cb\hat M=\sum_{a,b}M_{ab}c^\dagger_ac_b and exp⁡\exp the power-series exponential of matrices,

  1. exp⁡(itM^) ∣0⟩=∣0⟩\exp(it\hat M)\,|0\rangle=|0\rangle, and
  2. exp⁡(itM^)  cγ†  exp⁡(−itM^)=∑a=0K−1(exp⁡(itM))aγ ca†\exp(it\hat M)\;c^\dagger_\gamma\;\exp(-it\hat M)=\sum_{a=0}^{K-1}\bigl(\exp(itM)\bigr)_{a\gamma}\,c^\dagger_a.

The first exponential acts on the 2K2^K-dimensional Fock space, the last one is the K×KK\times K matrix exponential.

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