Prove2Me

Canonical anticommutation relations (Eq. (15))

Proved
KochHF.canonical_anticommutation

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

hartree-fockmathematical-physicssecond-quantization

For all orbitals φ,χ∈CK\varphi,\chi\in\mathbb C^K the creation and annihilation operators of Fock space satisfy the defining relations (15):

(cφ†)†=cφ,{cφ,cχ}=0={cφ†,cχ†},{cφ,cχ†}=⟨φ∣χ⟩,(c^\dagger_\varphi)^\dagger=c_\varphi,\qquad \{c_\varphi,c_\chi\}=0=\{c^\dagger_\varphi,c^\dagger_\chi\},\qquad \{c_\varphi,c^\dagger_\chi\}=\langle\varphi|\chi\rangle, cφ∣0⟩=0,⟨0∣0⟩=1,c_\varphi|0\rangle=0,\qquad\langle0|0\rangle=1,

where {A,B}=AB+BA\{A,B\}=AB+BA (Eq. (14)).

These relations are the postulates from which all of second quantization in the source is derived; in the finite model they become a theorem about the explicit operators.

Preamble
import Mathlib
import Definitions.Def_KochHF_FockSpace

open Matrix
Formal statement
namespace KochHF

theorem canonical_anticommutation {K : ℕ} (φ χ : Fin K → ℂ) :
    (cdagOrb φ)ᴴ = cannOrb φ ∧
    cannOrb φ * cannOrb χ + cannOrb χ * cannOrb φ = 0 ∧
    cdagOrb φ * cdagOrb χ + cdagOrb χ * cdagOrb φ = 0 ∧
    cannOrb φ * cdagOrb χ + cdagOrb χ * cannOrb φ = orbInner φ χ • (1 : FockOp K) ∧
    cannOrb φ *ᵥ vacuum K = 0 ∧
    fockInner (vacuum K) (vacuum K) = 1 := 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.1, p. 2.6, Eqs. (14), (15) (and (16) for general orbitals).
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 every KK and every φ,χ∈CK\varphi,\chi\in\mathbb C^K, all of the following hold simultaneously:

  1. the conjugate transpose of cφ†c^\dagger_\varphi equals cφc_\varphi;
  2. cφcχ+cχcφ=0c_\varphi c_\chi+c_\chi c_\varphi=0;
  3. cφ†cχ†+cχ†cφ†=0c^\dagger_\varphi c^\dagger_\chi+c^\dagger_\chi c^\dagger_\varphi=0;
  4. cφcχ†+cχ†cφ=⟨φ∣χ⟩⋅1c_\varphi c^\dagger_\chi+c^\dagger_\chi c_\varphi=\langle\varphi|\chi\rangle\cdot\mathbb 1, with 1\mathbb 1 the identity on Fock space;
  5. cφ∣0⟩=0c_\varphi|0\rangle=0;
  6. ⟨0∣0⟩=1\langle 0|0\rangle=1.

No hypotheses on φ,χ\varphi,\chi (they may be zero or non-normalized); K=0K=0 is allowed (Fock space is then one-dimensional).

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