First-order energy variation under $e^{i\lambda\hat M}$ (Eqs. (61), (62))

Proved

KochHF.energy_variation_first_order

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

hartree-fockmathematical-physicssecond-quantization

Let $\hat H$ be any operator on Fock space, $|\Phi\rangle=c^\dagger_{\alpha_N}\cdots c^\dagger_{\alpha_1}|0\rangle$ a Slater determinant, $M$ a hermitian $K\times K$ matrix and

E(\lambda)=\langle\Phi|e^{i\lambda\hat M}\,\hat H\,e^{-i\lambda\hat M}|\Phi\rangle .

Then $E$ is differentiable at $\lambda=0$ with

E'(0)=i\,\langle\Phi|[\hat M,\hat H]|\Phi\rangle .

Hence the energy functional is stationary under all such variations exactly when $\langle\Phi|[\hat H,\hat M]|\Phi\rangle=0$ for every hermitian $M$ (Eq. (62)).

Formalization Note The source's Eq. (61) prints the first-order term as $i\lambda\langle\Phi|[\hat H,\hat M]|\Phi\rangle$ ; differentiating $e^{i\lambda\hat M}\hat He^{-i\lambda\hat M}$ gives $i[\hat M,\hat H]=-i[\hat H,\hat M]$ . The statement uses the correct sign; the stationarity condition (62) is unaffected.

Preamble

import Mathlib
import Definitions.Def_KochHF_FockSpace

open Matrix

Formal statement

namespace KochHF

theorem energy_variation_first_order {K N : ℕ} (H : FockOp K) (α : Fin N → Fin K → ℂ)
    (M : Matrix (Fin K) (Fin K) ℂ) (hM : M.IsHermitian) :
    HasDerivAt
      (fun t : ℝ => matEl (slater α)
        (NormedSpace.exp ((Complex.I * t) • oneBodyOp M) * H *
          NormedSpace.exp ((-(Complex.I * t)) • oneBodyOp M)) (slater α))
      (Complex.I * matEl (slater α) (oneBodyOp M * H - H * oneBodyOp M) (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, p. 2.17, Eqs. (61), (62).

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,N$ , every Fock-space operator $H$ (no hermiticity assumed), every family $\alpha_0,\dots,\alpha_{N-1}\in\mathbb C^K$ (no orthonormality assumed), and every hermitian $K\times K$ matrix $M$ : the function $E:\mathbb R\to\mathbb C$ ,

E(t)=\langle\Phi_\alpha|\,\exp(it\hat M)\,H\,\exp(-it\hat M)\,|\Phi_\alpha\rangle,

has derivative at $t=0$ equal to

i\,\langle\Phi_\alpha|\,(\hat MH-H\hat M)\,|\Phi_\alpha\rangle .

(The statement asserts that this derivative exists and has this value.)

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

First-order energy variation under eiλM^e^{i\lambda\hat M}eiλM^ (Eqs. (61), (62))

First-order energy variation under $e^{i\lambda\hat M}$ (Eqs. (61), (62))