Canonical restricted MP2 specification¶
This extension proves selected scalar identities used in the closed-shell canonical MP2 contraction. Numerical checks passed for the case below. It does not yet prove perturbation theory, the AO-to-MO transform, or the full indexed sum. UMP2, RI-MP2, local approximations and periodic MP2 remain separate obligations.
Amplitudes and spin components¶
Start from a stationary canonical RHF reference with integer occupations. The MP partition uses the Fock operator as the unperturbed one-electron operator. Doubly excited determinants supply the second-order correction; Brillouin’s theorem removes the singles contribution. Those statements are physical/mathematical inputs to this pilot, not results proved in Lean here. For occupied \(i,j\) and virtual \(a,b\), define
The implemented spatial-orbital expressions are
mp2_spin_decomposition proves the OS+SS summand identity.
mp2_same_spin_pair proves that adding the exchanged contribution yields
\((x-y)^2/\Delta\). To extend this identity to an SS sum requires the exchange
permutation to preserve the summation domain and denominator; that finite-sum
reindexing proof is outstanding. The factor one-half must be included when
averaging the two equivalent sums.
mp2_amplitude_equation proves \(\Delta(g/\Delta)=g\) under \(\Delta\ne0\).
mp2_gapped_denominator proves negativity from
\(\epsilon_i<\epsilon_a\) and \(\epsilon_j<\epsilon_b\).
mp2_square_term_nonpositive proves \(g^2/\Delta\le0\) for a negative denominator.
A finite nonzero denominator alone does not establish perturbative reliability.
The algebraic identities at Lean’s totalized division by zero do not authorize
using a singular MP2 denominator; physical amplitudes require the nonzero premise.
Implementation correspondence¶
cpp/src/mp2.cpp::accumulate_incore evaluates the two sums with a shared
energy denominator, and applies configurable spin scaling afterwards.
check_extensions.py transforms
native AO ERIs independently with NumPy, uses the returned RHF orbitals and
energies, and compares OS, SS and total correlation energies with run_mp2.
It uses water/STO-3G at the RHF geometry, explicitly sets
n_frozen_core=0 and density_fit=False, and requires all denominators negative.
Its negative controls reverse the denominator sign and omit exchange.
The component tolerance is \(2\times10^{-10}\) hartree; independent reference
acceptance will use \(10^{-8}\) hartree for the total energy with matched settings.
References: Moller and Plesset (1934), DOI; Helgaker, Jorgensen and Olsen, Sections 14.2.4-14.2.5 and 14.4, DOI. The original perturbation theory and the explicit spin-orbital second-order expression motivate the working formula; their complete derivations are not claimed as checked Lean proofs.
Measured acceptance¶
On 1 November 2026, the same 0.18.5 source runtime recorded on the
UHF page gave OS=-0.03244050438115507 and
SS=-0.001960293169478777 hartree. The independently reconstructed
correlation energy agreed with the native result within \(1.388\times10^{-17}\)
hartree. The total energy was -74.99473786659992 hartree, compared with
ORCA 6.1.1’s -74.994737866670 hartree: an absolute difference of
\(7.008\times10^{-11}\) hartree, within the preset \(10^{-8}\) criterion.
The matched input is reference_water_mp2.inp.