Prove2Me

Electron-hole excitation energy εb−εa−Δab\varepsilon_b-\varepsilon_a-\Delta_{ab} (Eq. (67))

Proved
KochHF.electron_hole_excitation_energy

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

hartree-fockmathematical-physicssecond-quantization

With H^\hat H, TT, UU as in the definition file and Unn′,mm′=Un′n,m′mU_{nn',mm'}=U_{n'n,m'm}, let SS be the occupied reference orbitals, a∈Sa\in S and b∉Sb\notin S. The energy of the determinant with an electron moved from aa to bb satisfies

⟨Sa→b∣H^∣Sa→b⟩−⟨S∣H^∣S⟩=εb−εa−Δab,Sa→b=(S∖{a})∪{b},\langle S_{a\to b}|\hat H|S_{a\to b}\rangle-\langle S|\hat H|S\rangle=\varepsilon_b-\varepsilon_a-\Delta_{ab},\qquad S_{a\to b}=(S\setminus\{a\})\cup\{b\},

with εm=Tmm+∑m′∈SΔmm′\varepsilon_m=T_{mm}+\sum_{m'\in S}\Delta_{mm'} the orbital energies of SS.

The term −Δab-\Delta_{ab} is the electron-hole interaction of the unrelaxed particle-hole excitation.

Preamble
import Mathlib
import Definitions.Def_KochHF_FockSpace
import Definitions.Def_KochHF_Hamiltonian

open Matrix
Formal statement
namespace KochHF

theorem electron_hole_excitation_energy {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)) (a b : Fin K) (ha : a ∈ S) (hb : b ∉ S) :
    detEnergy T U (insert b (S.erase a)) - detEnergy T U S =
      hfOrbitalEnergy T U S b - hfOrbitalEnergy T U S a - hfDelta U a b := 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.18, Eq. (67).
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 complex K×KK\times K matrix TT, every complex 4-index array UU with Unn′mm′=Un′nm′mU_{nn'mm'}=U_{n'nm'm} for all indices, every S⊆{0,…,K−1}S\subseteq\{0,\dots,K-1\}, every a∈Sa\in S and every b∉Sb\notin S:

E((S∖{a})∪{b})−E(S)=εbS−εaS−(Uabab−Uabba),E\bigl((S\setminus\{a\})\cup\{b\}\bigr)-E(S)=\varepsilon^S_b-\varepsilon^S_a-\bigl(U_{abab}-U_{abba}\bigr),

where E(R)=⟨R∣H^(T,U)∣R⟩E(R)=\langle R|\hat H(T,U)|R\rangle and εmS=Tmm+∑m′∈S(Umm′mm′−Umm′m′m)\varepsilon^S_m=T_{mm}+\sum_{m'\in S}(U_{mm'mm'}-U_{mm'm'm}), both orbital energies computed with the original set SS.

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