vibe-qc/Documentation

Real finite-basis RHF derivation and proof scope

The RHF pilot covers the algebra of a real, spin-summed, closed-shell density, the conventional Coulomb/exchange contractions, the finite-basis electronic energy and its directional derivative, and the stationarity identity implied by the Roothaan equations. The Lean source and numerical checker use the same explicit index convention. The correspondence to native C++ is tested.

Scope and assumptions

The physical setting is the nonrelativistic Born-Oppenheimer electronic Hamiltonian in atomic units, with fixed nuclei and a finite real AO basis. The pilot uses integer double occupation, conventional four-centre integrals, and no ECP, XC functional, dispersion, solvation or additional energy term.

The reference is Helgaker, Jorgensen and Olsen, Molecular Electronic-Structure Theory (2000), doi:10.1002/9781119019572: Section 10.6.1, equations (10.6.2), (10.6.16)-(10.6.18), and Sections 10.7.1-10.7.3, particularly (10.7.23)-(10.7.27). Their scaled density in Section 10.7.3 is half the spin-summed density used below. Their exchange ordering and vibe-qc’s ordering are equivalent for a symmetric density and real ERIs with the stated permutation symmetries.

The Slater-determinant expectation value supplies the starting energy. The continuum Hamiltonian, determinant integration and the Gaussian integral evaluator are not formalized in this pilot. The mathematical theorems start from finite real arrays and their explicit symmetries. No floating-point rounding bound or general SCF convergence theorem is asserted.

Orbitals and the density metric

Let \(\chi_\mu\) be the AOs and \(S_{\mu\nu}=\langle\chi_\mu|\chi_\nu\rangle\). With \(m=N_e/2\) occupied spatial orbitals,

\[ \phi_i=\sum_\mu\chi_\mu C_{\mu i},\qquad C_o^T S C_o=I_m,\qquad D=2C_oC_o^T. \]

Here \(C_o\) has shape \(n_{\rm AO}\times m\) and contains only occupied columns. In Lean, AO and occupied indices are distinct finite types. Matrix products must have compatible domains. The density is symmetric because transposition reverses the product twice. Its electron count follows by cycling the trace:

\[ \operatorname{Tr}(DS)=2\operatorname{Tr}(C_oC_o^TS) =2\operatorname{Tr}(C_o^TSC_o)=2m. \]

The corresponding idempotency relation is

\[ DSD=4C_o(C_o^TSC_o)C_o^T=4C_oC_o^T=2D. \]

The overlap matrix is essential; \(D^2=2D\) holds in an orthonormal basis, not in a general AO basis. For any occupied-space orthogonal matrix with \(UU^T=I_m\), \(D(C_oU)=D(C_o)\). These identities need the stated orbital orthonormality, but do not require an invertible full AO overlap matrix. They also apply after restricting to a retained linearly independent space.

Integral conventions and the Fock matrix

For real basis functions, write chemists’ ERIs as

\[ g_{\mu\nu\lambda\sigma}=(\mu\nu|\lambda\sigma). \]

The explicit hypotheses are pair interchange and interchange within each pair:

\[ g_{\mu\nu\lambda\sigma}=g_{\lambda\sigma\mu\nu},\quad g_{\mu\nu\lambda\sigma}=g_{\nu\mu\lambda\sigma},\quad g_{\mu\nu\lambda\sigma}=g_{\mu\nu\sigma\lambda}. \]

With \(h=T+V_{\rm ne}\), vibe-qc uses

\[ J[D]_{\mu\nu}=\sum_{\lambda\sigma}D_{\lambda\sigma}g_{\mu\nu\lambda\sigma}, \qquad K[D]_{\mu\nu}=\sum_{\lambda\sigma}D_{\lambda\sigma}g_{\mu\lambda\nu\sigma}, \]

\[ G[D]=J[D]-\tfrac12K[D],\qquad F[D]=h+G[D]. \]

The one-half exchange coefficient is required because \(D\) already sums both spins. Flattening the ordered AO pair to \(p=(\mu,\nu)\) gives the linear map

\[ W_{p q}=g_{\mu\nu\lambda\sigma} -\tfrac12g_{\mu\lambda\nu\sigma},\qquad G[D]=WD. \]

Lean proves the equivalence of these indexed contractions and the flattened map. The ERI symmetries imply \(W_{pq}=W_{qp}\), hence \(\langle A,G[B]\rangle=\langle B,G[A]\rangle\). Here \(\langle A,B\rangle=\sum_{\mu\nu}A_{\mu\nu}B_{\mu\nu}\) is the real Frobenius inner product. Symmetric \(h,D\) and the ERI symmetries also give a symmetric Fock matrix.

Electronic energy and its derivative

The closed-shell determinant energy in occupied orbitals is

\[ E=E_{\rm nuc}+2\sum_i h_{ii}+\sum_{ij}[2(ii|jj)-(ij|ji)]. \]

Substitution of \(D=2C_oC_o^T\) gives the AO working expression

\[ E_{\rm el}[D]=\langle D,h\rangle+\tfrac12\langle D,G[D]\rangle =\tfrac12\langle D,h+F[D]\rangle. \]

The first equality is the finite-basis energy definition used in Lean; the half-Fock identity is proved from that definition. For symmetric matrices the Frobenius product equals the corresponding trace expression. This is also the elementwise contraction used by the native RHF driver.

Linearity and reciprocity of \(G\) give the exact identity, for any real \(t\),

\[ E_{\rm el}[D+tX]=E_{\rm el}[D] +t\langle X,F[D]\rangle+\frac{t^2}{2}\langle X,G[X]\rangle. \]

Lean proves both this polynomial identity and its derivative at \(t=0\):

\[ \left.\frac{d}{dt}E_{\rm el}[D+tX]\right|_{t=0}=\langle X,F[D]\rangle. \]

An unconstrained matrix direction \(X\) need not remain a physical determinant density. The identity is about the polynomial energy on its full array domain; orbital constraints enter the following variational argument.

Roothaan equations and stationarity

For a real orbital variation, \(\delta D=2(\delta C_oC_o^T+C_o\delta C_o^T)\). Using symmetric \(F\), the energy variation becomes \(\delta E=4\langle FC_o,\delta C_o\rangle\). Introduce the Lagrangian

\[ \mathcal L(C_o)=E(C_o)-2\operatorname{Tr} [\Lambda(C_o^TSC_o-I)],\qquad\Lambda^T=\Lambda. \]

Its stationary equation is \(FC_o=SC_o\Lambda\). An orthogonal occupied-space rotation diagonalizes \(\Lambda\) without changing \(D\), producing \(FC_o=SC_o\varepsilon_o\). This orbital variational derivation is written here; the pilot does not yet formalize the orbital chain rule or the full constrained-minimization theorem.

The following consequence of a generalized occupied eigenpair is proved in Lean. If \(S,F,\varepsilon_o\) are symmetric, transposing the eigen-equation gives \(C_o^TF=\varepsilon_o C_o^TS\), and therefore

\[ FDS=2SC_o\varepsilon_o C_o^TS=SDF. \]

Thus the metric commutator vanishes at such a stationary solution. The theorem does not assert that an SCF algorithm reaches that solution or that it is a local or global minimum.

Theorems and implementation correspondence

The proof files are Density.lean and Energy.lean.

Lean declaration in VibeQCRHF	Claim	Implementation/check
density_symmetric	\(D^T=D\)	cpp/src/rhf.cpp::build_density; returned density
density_metric_idempotent	\(DSD=2D\)	Occupied coefficients, overlap and returned density
density_electron_count	\(\operatorname{Tr}(DS)=2m\)	Electron count in the same nonorthogonal metric
density_occupied_rotation	\(D(C_oU)=D(C_o)\)	Synthetic occupied-space rotations
roothaan_implies_stationarity	\(FC_o=SC_o\varepsilon_o\) implies \(FDS=SDF\)	Native returned Fock, coefficients and density
rhfKernel_symmetric	The interaction kernel is reciprocal	Random real ERIs with all required symmetries
coulomb_contraction	Ordered-pair map equals indexed J	cpp/src/fock.cpp::build_coulomb
exchange_contraction	Ordered-pair map equals indexed K	cpp/src/fock.cpp::build_exchange
rhf_contraction	\(G=J-K/2\)	cpp/src/fock.cpp::build_fock_g
energy_half_fock	Half-Fock energy equals the quadratic energy	Native RHF e_electronic
interaction_reciprocal	\(\langle A,G[B]\rangle=\langle B,G[A]\rangle\)	Native G evaluated at two densities
energy_expansion	Exact second-order energy expansion	Native G at perturbed densities
energy_directional_derivative	Derivative for a symmetric interaction map	Central finite differences of the native-G energy
rhf_energy_directional_derivative	Instantiate the derivative with the RHF ERIs	Same test with symmetry-preserving ERIs
rhf_fock_symmetric	Symmetric h and D produce symmetric F	Native Fock matrices

cpp/include/vibeqc/integrals.hpp defines the dense ERI layout as ((i*n+j)*n+k)*n+l. cpp/src/bindings.cpp exposes the native J, K and G builders to the checker. cpp/src/rhf.cpp evaluates the energy using the Fock matrix built from the corresponding density, before DIIS extrapolation, and rebuilds the final reported energy. The pilot exercises the conventional route; direct screening, RI and COSX require their own correspondence checks.

Reproducible numerical checks

check_rhf.py independently evaluates the indexed expressions with NumPy and calls the imported native builders. The deterministic synthetic cases use 1, 2, 3, 5 and 8 AOs, positive-definite nonidentity overlaps and real ERIs formed from symmetric factors. The checker compares J, K, G, reciprocity, energy expansions and finite differences, with absolute tolerances of \(2\times10^{-10}\) for algebraic tests and \(2\times10^{-8}\) for the finite-difference derivative.

Six negative controls must be rejected: a missing density factor of two, an omitted overlap metric, exchange coefficient one, a positive exchange sign, a permuted ERI layout and a missing energy factor of one-half. These are deliberately altered candidate values, not changes to the installed code.

The full calculation uses water/STO-3G, charge zero and multiplicity one, with positions in bohr:

O  0.0  0.0  0.0
H  0.0  1.4  1.1
H  0.0 -1.4  1.1

It uses conventional RHF, no density fitting, a core-Hamiltonian initial guess, energy convergence \(10^{-12}\) hartree and gradient convergence \(10^{-10}\). The check requires convergence and tests the returned density, Fock, generalized eigen-equation, commutator and total/electronic energies. The independent reference input is reference_h2o.inp.

Measured pilot results

The 1 November 2026 validation used vibe-qc 0.18.5, source revision 006069bd8c005aa32ca60c60814f7cf50ef1b25e, and ORCA 6.1.1 with the matched input above. The conventional RHF driver and J/K builder source were unchanged between that runtime and the source revision used for this pilot. Water converged in nine vibe-qc iterations.

Quantity	Measured result
vibe-qc total energy / hartree	-74.96033706904929
ORCA total energy / hartree	-74.960337068945
Absolute energy difference / hartree	\(1.043\times10^{-10}\)
Required cross-code agreement / hartree	\(10^{-8}\)
Largest J/K/G comparison residual	\(5.330\times10^{-15}\)
Largest metric-idempotency residual	\(6.218\times10^{-15}\)
Largest directional-derivative residual	\(8.516\times10^{-12}\)
Roothaan-equation residual	\(1.422\times10^{-14}\)
Metric-commutator residual	\(6.218\times10^{-15}\)
Deliberate errors detected	6 of 6

Residuals are maximum absolute entrywise differences; rows labelled “largest” include all five synthetic cases and the molecular checks where applicable. They are measured errors for these cases, not general error bounds. The native module SHA-256 was 32e0a0d9a27e9ec3bd6fc3bb9f782cf2638c0ee5f6d69575226ec2054a0267df. The separate Lean 4.35.0 build and transitive-axiom audit passed for all 15 listed theorems, with only propext, Classical.choice and Quot.sound.

See mathematical verification for reproduction commands, the trust boundary and the distinction between proofs, numerical implementation checks and scientific validation.