TheoremStatement: AI-adaptedProof: AI-generatedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Residual-certified DIIS candidates inherit the contractive SCF error budget

Statement

Assume the hypotheses and certificates in Finite-budget certified SCF with safeguarded DIIS and a contractive fallback: $Φ$ is a $q$ -contraction on the complete invariant set $K$ , its fixed point is $P_{*}$ , the starting error is at most $E_{0}$ , and every baseline response error is at most $η_{k}$ . Let $E_{k}$ be updated by that algorithm. Then every produced iterate obeys $∥ P_{k} - P_{*} ∥_{F} \leq E_{k} \leq q^{k} E_{0} + \sum_{j = 0}^{k - 1} q^{k - 1 - j} η_{j} .$ An accepted DIIS candidate has certified error at most $q E_{k}$ ; the commutator least-squares residual alone is not used as an error bound. If an infinite sequence of updates follows these rules, with a valid baseline fallback whenever a candidate is rejected and fallback error budgets $η_{k} \to 0$ , then $P_{k} \to P_{*}$ . A finite execution of the stated algorithm may still return budget exhaustion. Use the convention $q^{0} = 1$ , including when $q = 0$ .

Facts & Assumptions

Given: The certified algorithm's hypotheses, starting error bound $E_{0}$ , contraction factor $0 \leq q < 1$ , and nonnegative baseline error budgets $η_{k}$ .

[F1]

For every $X \in K$ , $∥ X - P_{*} ∥_{F} \leq ∥ X - Φ (X) ∥_{F} / (1 - q)$ (A contractive self-consistent map converges and admits residual and inexact-solve bounds).

[F2]

A DIIS candidate is accepted only when its certified residual bound divided by $1 - q$ is at most $q E_{k}$ ; otherwise the baseline update is used and its error bound is added to $q E_{k}$ (Finite-budget certified SCF with safeguarded DIIS and a contractive fallback).

Proof

1.1givenF1F2

Initially $∥ P_{0} - P_{*} ∥_{F} \leq E_{0}$ by input. Suppose $∥ P_{k} - P_{*} ∥_{F} \leq E_{k}$ . If the algorithm accepts candidate $Y = P_{k + 1}$ , [F2] gives a certified upper bound $\overset{ˉ}{ρ} (Y)$ for $∥ Y - Φ (Y) ∥_{F}$ with $\overset{ˉ}{ρ} (Y) / (1 - q) \leq q E_{k}$ . Applying [F1] at $Y$ proves $∥ P_{k + 1} - P_{*} ∥_{F} \leq q E_{k} = E_{k + 1}$ .

2.1givenstep 1.1F2algebra

If the baseline is used, its evaluator certifies $∥ P_{k + 1} - Φ (P_{k}) ∥_{F} \leq η_{k}$ . The triangle inequality and contraction give $∥ P_{k + 1} - P_{*} ∥_{F} \leq η_{k} + ∥ Φ (P_{k}) - Φ (P_{*}) ∥_{F} \leq η_{k} + q ∥ P_{k} - P_{*} ∥_{F} \leq q E_{k} + η_{k} = E_{k + 1} .$ Thus induction proves $∥ P_{k} - P_{*} ∥_{F} \leq E_{k}$ at every step.

3.1step 2.1F2inductionalgebra

By [F2], both update branches obey $E_{k + 1} \leq q E_{k} + η_{k}$ (accepted DIIS uses $η_{k} = 0$ for this upper estimate). Iterating this scalar recurrence by induction gives $E_{k} \leq q^{k} E_{0} + \sum_{j < k} q^{k - 1 - j} η_{j}$ .

4.1givenstep 2.1step 3.1algebra∎

For any infinite sequence generated by the stated update rules with $η_{j} \to 0$ , the scalar recurrence from step 3.1 has convolution tending to zero: for $0 < q < 1$ and any $ϵ > 0$ , choose $J$ so $η_{j} \leq (1 - q) ϵ / 2$ for $j \geq J$ . The tail sum is at most $ϵ / 2$ , while the finite head and $q^{k} E_{0}$ tend to zero as $k \to \infty$ . If $q = 0$ , the recurrence gives $E_{k + 1} \leq η_{k} \to 0$ directly. Thus $E_{k} \to 0$ and step 2.1 gives $P_{k} \to P_{*}$ . This is a conditional statement about an infinite sequence; it does not assert that a finite-budget run must meet its stopping tolerance.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

8 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Thorsten Rohwedder, An analysis for some methods and algorithms of quantum chemistry, Chapter 4 §4.4 (standard reference, not scraped)
Eric Cancès, Gaspard Kemlin, and Antoine Levitt, Convergence analysis of direct minimization and self-consistent iterations, §3.2 (standard reference, not scraped)