Formal in Silico — mini-DFT

Claims in the trust ledger

Of the ledger’s 132 claims, 102 concern mini-DFT; they are grouped below by topic. The tiers are defined on the programme page.

T4 end to end · 20 T3 machine proof · 74 T2 model-checked · 2 T0 tested · 1 target not yet reached · 5

DFT foundations

discrete model · algorithm · parallelism · floating point

Ground-state energy certificate

Finite-temperature free energy

Gaussian and cold smearing

SCF-solution certificates

Methfessel–Paxton · Marzari–Vanderbilt

k-point sampling and supercells

Discretisation error

truncation K → ∞ · true Gaussian potential

Density and eigenvalues

Band structure and density of states

LDA exchange (Slater)

exchange on a real-space grid · nonlinear SCF-solution certificates · energy

The T4 claims are the soundness theorems of the certificate checkers (which run in exact rational arithmetic, so no floating point is involved) and the proof that the trusted C kernel has no run-time errors. The five claims below target: continuum well-posedness of 1D rHF, the a priori plane-wave estimate and linear-mixing convergence (all awaiting a literature check at T1), the equality of the truncation limit with the continuum energy, and the Lean–Rocq interface claim.

Goal G1 — mini-DFT reaches DFTK parity

Reference: DFTK.jl 0.8.0 on the same discrete problem. Order: complete the 1D feature set (M0–M3), generalise the Lean model to d dimensions for 2D/3D (M4–M5), then infrastructure (M6).

Done — implemented, agrees, certified Agrees — certificates incomplete Implemented — not yet compared Not started

Existing core

5 / 9

1D solvers, occupation, k-points

1 / 7

1D physics terms

0 / 7

1D post-processing and response

0 / 9

d dimensions

0 / 7

Full 3D

0 / 4

Infrastructure and interfaces

0 / 3

M0 · existing core

Feature	Status	What is certified
Kinetic, external (Fourier) and Hartree terms	Done	Ground-state energy, density, eigenvalues and each energy component
Fermi–Dirac smearing and entropy	Done	Free energy, entropy and energy; existence of the finite-temperature ground state and uniqueness of its density are proved
Γ-centred grids with an odd number of k-points	Done	Per-cell energy through the equivalent supercell, plus its truncation limit
Even grids, Monkhorst–Pack	Done	Supercell with half-integer frequencies; grids that contain the zone boundary are excluded
Dense diagonalisation	Done	Each eigenpair enclosed by a residual bound; Sylvester inertia confirms they are the lowest ones
Linear, Kerker and Anderson mixing	Implemented	Does not affect the result, which is checked by certificate
Non-self-consistent bands, Gaussian-broadened DOS	Agrees	Certified for zero-temperature Γ-point runs; finite-temperature and k-point runs not yet
Supercells	Implemented	Supercell equivalence is proved
Parallelism over k-points	Implemented	Threads rather than MPI; the protocol is model-checked (T2), results are bitwise identical across thread counts

M1 · 1D solvers, occupation and k-points

Feature	Status	What is certified
Gaussian, Methfessel–Paxton, Marzari–Vanderbilt smearing	Agrees Gaussian done	Gaussian: free energy, entropy and energy. MP and MV occupations can exceed 1, so there is no variational principle; instead the checker proves that the discrete SCF equations have exactly one solution near the computed one, bounds its chemical potential, and encloses its energy and free energy (free-energy interval about 5×10⁻¹⁴ wide). DFTK’s Fermi level, energy and free energy all fall inside the Lean intervals. Missing: higher-order MP.
Monkhorst–Pack grids, shifts, time-reversal reduction	Done	Every grid without the zone boundary is certified; DFTK’s energies lie inside the Lean intervals
Bands and DOS aligned with DFTK	Agrees	As in M0
Grid-based Hamiltonian action, LOBPCG, preconditioning	Not started	Alias-free grid action is already proved
Adaptive band count and diagonalisation tolerance	Not started
LDOS, dielectric and χ₀ mixing; potential mixing	Not started
Newton’s method, direct minimisation	Not started

M2 · 1D physics terms

Feature	Status	What is certified
LDA exchange-correlation (Slater exchange, PW92 correlation)	Agrees	Evaluated on the same real-space grid as DFTK (M = 4K + 1 points); six systems — zero temperature, Fermi–Dirac, Marzari–Vanderbilt, Gaussian with Monkhorst–Pack k-points, bands and DOS — agree with DFTK in energy, every component and every eigenvalue. The energy is no longer convex, so there is no variational certificate; for Slater exchange at the Γ point with MV or first-order MP smearing, the checker proves that the nonlinear SCF equations have exactly one solution within about 10⁻¹² of the computed one and encloses its chemical potential, energy (exchange included) and free energy (DFT-X01–X13). DFTK’s Fermi level, energy and free energy fall inside the Lean intervals. Missing: PW92 correlation, zero temperature, Fermi–Dirac and Gaussian smearing, k-points.

Planned: M2–M6 (29 items not started)

M2 · 1D physics terms

Collinear spin (LSDA), magnetic term
Local nonlinearity (Gross–Pitaevskii)
Exact exchange (Hartree–Fock, hybrids)
Atoms and pseudopotentials: local and nonlocal parts, Ewald, correction terms
Pairwise interatomic potentials
DFT+U

M3 · 1D post-processing and response

Forces
Geometry optimisation
Stresses
Response: χ₀, Hessian, DFPT
Polarisability
Phonons
Elastic constants
A posteriori error estimates and refinement
Currents

M4 · d dimensions

Lean model generalised to d-dimensional lattices
2D/3D plane waves with FFTW
Arbitrary lattices, atomic structures, symmetry
HGH and UPF pseudopotentials
3D Ewald and pseudopotential correction
Anyons (2D)
DFTK examples: silicon, graphene, GaAs surface, Cohen–Bergstresser

M5 · full 3D

GGA and meta-GGA
3D forces, stresses, phonons, elastic constants
Exact exchange (ACE)
MPI k-point parallelism, bitwise identical on 1–64 processes

M6 · infrastructure (last; may be trimmed)

GPU
Arbitrary floating-point types, automatic differentiation
Wannier90, VTK, JSON and plotting interfaces

What a certified run reports today

Rigorous intervals for

the discrete ground-state energy, and the truncation limit with a bound on the discretisation error
the energy under the true Gaussian potential, Fourier tail included
the ground-state density (Coulomb norm and pointwise) and the Hartree potential
every eigenvalue of the ground-state Hamiltonian, and the gap
kinetic, external and Hartree energy components
band energies along a path and density-of-states values
free energy, entropy and energy at finite temperature
for MP/MV smearing: a locally unique SCF solution, its chemical potential, energy and free energy
for LDA (Slater exchange) with MP/MV smearing: a locally unique solution of the nonlinear SCF equations, its chemical potential, energy including the exchange energy, and free energy
per-cell values for k-point runs, through the equivalent supercell

Cross-checks and supporting evidence

Benchmarks do not raise a tier, but they catch misunderstandings: a Lean interval that excludes an independent reference value would reveal a wrong model.

DFT benchmark suite, including cross-checks with DFTK.jl (run of 1 October)143 / 143 pass
Energies (free energies) against DFTK.jl on the same discrete problem≤ 5×10⁻¹⁵
All eigenvalues and energy components against DFTK.jl≤ 10⁻¹²
DFTK’s Gaussian free energy, and its MP/MV Fermi level, energy and free energyinside the Lean intervals
LDA against DFTK.jl with the same grid: energies, components including exchange-correlation, eigenvalues (six systems); for certified LDA runs DFTK’s Fermi level, energy and free energyagree; inside the Lean intervals
LDA SCF-solution certificate, K = 8 (Marzari–Vanderbilt): radius of uniqueness / energy interval / free-energy interval / checking time4×10⁻¹² / 1×10⁻⁸ / 2×10⁻¹⁵ / 6 s
Reports with 1, 2, 4 and 7 threadsbitwise identical
Trace validation: runs ending converged, gap closed, max iterations, certificate failedall accepted
Trace validation: tampered traces (claimed convergence without a certificate, a dropped record, wrong limit)all rejected
Mutation tests on the SCF controller spec (remove the certificate check or the iteration cap)caught by TLC
Trace validation of the k-point threads: every claim, join and reduction step replayed against the protocol, 1, 4 and 7 threadsall accepted
Tampered thread logs (double claim, claim out of counter order, reduction out of order, join before exit, missing chemical-potential step)all rejected
Report validation: every Lean line in a report is the checker’s own output; a rejecting, crashing or missing checker makes the driver exit with an errorpass
Fuzzing of the driver under AddressSanitizer and UBSan (about 4 000 mutated inputs), after hardening its input parsingno memory errors, undefined behaviour or crashes

Open gaps

An output without a Lean theorem is unfinished. These are the ones we know about, listed rather than hidden.

k-point sums versus the infinite crystalEach k-point run is certified for its own discrete problem, but the error of the k-point sum relative to the infinite crystal has no bound yet; k-point energies are not variational.
Grids containing the Brillouin-zone boundaryNo certificate; DFTK’s treatment there is also a different discrete problem, so neither side is compared.
Higher-order Methfessel–Paxton, and scaling of SCF-solution certificatesChecking time grows roughly with the fourth power of the supercell size; for gapped systems with the chemical potential mid-gap the SCF equations are ill-conditioned and the certificate honestly fails; uniqueness is only local.
LDA beyond Slater exchange at Γ with MP/MVPW92 correlation, zero temperature, Fermi–Dirac and Gaussian smearing and k-points agree with DFTK but have no certificate yet; the LDA energy interval is a first-order estimate, and only grids with M = 4K + 1 points are covered.
Discretisation error at finite temperatureCertified at zero temperature only.
Truncation limit equals the continuum energyNot yet proved.
Density, eigenvalues, bands and DOS for finite-temperature and k-point runsCertified for zero-temperature Γ-point runs only.
The problem written in the certificateThe potential coefficients, cell length, cutoff, electron count, temperature and smearing are written by the untrusted driver; the checker certifies exactly that problem but neither recomputes nor echoes it (A-DFT-05). Only the Gaussian-potential lines compare the coefficients with the true potential.
Code-level proof of the interval arithmeticThe Lean model and the C code agree by review and differential tests, not by proof.