Pipeline-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.

✓ 15 results · all verified · 3 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 12 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Gaussian basis integral recurrences and boys error

1 · Prerequisites

2 · Summary

This page defines finite Cartesian Gaussian primitives and contractions, then proves their Gaussian product, moment, derivative, and kinetic recurrences. The one- and two-electron Coulomb integrals are Lebesgue integrals; local integrability of the Coulomb singularities and Gaussian decay establish absolute convergence. A finite Hermite expansion reduces nuclear attraction and electron-repulsion terms to the Boys family and its auxiliary recurrence table.

The geometric convention for a pair of primitive exponents $a, b > 0$ is shown below in the one-dimensional projection along the segment joining $A$ to $B$ . The product center $P = (a A + b B) / (a + b)$ lies at fraction $b / (a + b)$ of the distance from $A$ to $B$ . The drawing uses the illustrative ratio $a : b = 13 : 7$ ; all integral identities are proved algebraically and do not rely on the picture.

\begin{tikzpicture}[>=stealth]
  \coordinate (A) at (0,0);
  \coordinate (B) at (6,0);
  \coordinate (P) at (2.1,0);
  \draw[thick] (A)--(B);
  \fill (A) circle (2pt) node[below] {$A$};
  \fill (P) circle (2pt) node[below] {$P=(aA+bB)/(a+b)$};
  \fill (B) circle (2pt) node[below] {$B$};
  \draw[<->] (0,0.55)--(2.1,0.55) node[midway,above] {$7/20$ of $|AB|$};
  \draw[<->] (2.1,0.55)--(6,0.55) node[midway,above] {$13/20$ of $|AB|$};
\end{tikzpicture}

For Boys evaluation, the small- $T$ branch uses a Taylor remainder only after its terms are decreasing; bounded arguments use a positive midpoint rule with a derivative enclosure; and large arguments use the scaled incomplete-gamma representation with a separate tail bound. Upward and downward recurrences carry explicit interval-radius amplification estimates. The finite evaluator chooses a direction from its computed bounds and may return inconclusive when its cap cannot certify the requested tolerance.

Each Boys seed binds its own order and receives finite child-call budgets. The integral algorithm fixes each auxiliary cutoff from the sum of the participating primitive angular degrees, deterministic update order, memoized pair and auxiliary tables, and a work counter. Coulomb screening operates on the input contracted basis, including every primitive contraction coefficient in its diagonal bounds, and uses the positive Coulomb form and Cauchy–Schwarz; all skipped energy contributions are accumulated in a reported bound. The separate tensor theorem gives energy and gradient error estimates with explicit basis size $n$ , contracted size $r$ , and coefficient norms. These are finite integral and tensor-contraction results; no Hartree–Fock postulate, universal recurrence stability, or exact-sparsity claim is made.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: AI-adaptedProof: Not applicableOpen item page →

Cartesian Gaussian primitives, contractions, and integral conventions

Definition

Write $N_{0} = {0, 1, 2, \dots}$ and $∥ x ∥_{2} = (x_{1}^{2} + x_{2}^{2} + x_{3}^{2})^{1 / 2}$ for $x \in R^{3}$ . For $α = (α_{1}, α_{2}, α_{3}) \in N_{0}^{3}$ , exponent $a > 0$ , and center $A \in R^{3}$ , a primitive Cartesian Gaussian is $g_{α, a, A} (x) = \prod_{j = 1}^{3} (x_{j} - A_{j})^{α_{j}} \exp (- a ∥ x - A ∥_{2}^{2}), x \in R^{3} .$ A finite Gaussian contraction is a finite sum $ϕ = \sum_{k = 1}^{q} c_{k} g_{α_{k}, a_{k}, A_{k}}$ with $q \in N_{0}$ , $c_{k} \in C$ , $a_{k} > 0$ , and $A_{k} \in R^{3}$ . The zero-term sum is the zero function. Bras are conjugated.

For a pair of contractions put $f_{ϕ, ψ} (x) = \overline{ϕ (x)} ψ (x)$ . For pair densities $f, g$ , define the Coulomb form $C (f, g) = \int_{R^{3}} \int_{R^{3}} \frac{\overline{f (x)} g (y)}{∥ x - y ∥_{2}} d y d x .$ For finite contractions $ϕ, ψ, ρ, σ$ , define the overlap, kinetic, point-nucleus attraction, and two-electron Coulomb expressions by $S (ϕ, ψ) = \int_{R^{3}} \overline{ϕ (x)} ψ (x) d x, T (ϕ, ψ) = - \frac{1}{2} \int_{R^{3}} \overline{ϕ (x)} Δ ψ (x) d x,$ $V_{C} (ϕ, ψ) = \int_{R^{3}} \frac{\overline{ϕ (x)} ψ (x)}{∥ x - C ∥_{2}} d x,$ $G (ϕ, ψ; ρ, σ) = C (f_{ϕ, ψ}, f_{ρ, σ}) .$ The primitives and their finite contractions are smooth: The exponential function is smooth and $(\exp)^{'} = \exp$ supplies smoothness of exp, and repeated coordinatewise applications of Sum, product, quotient, and chain rules from difference quotients supply all polynomial-product and composition derivatives. Thus the following Laplacian is well defined.

Here $Δ ψ = \sum_{j = 1}^{3} \partial_{x_{j}}^{2} ψ$ is the Cartesian Laplacian. All displayed integrals mean Lebesgue integrals in the sense of Integrable real and complex functions, and their integrals. A finite nuclear attraction is any finite real linear combination of the $V_{C}$ terms, with its centers and weights specified. This definition alone asserts neither convergence nor a physical approximation postulate.

Remarks

The exponents, centers, polynomial multi-indices, coefficients, and nuclear data are explicit finite input data. A contraction coefficient may be complex; later real variational energy bounds state their separate real-matrix hypotheses.

DefinitionDefinition: AI-adaptedProof: Not applicableOpen item page →

Boys functions and lower incomplete-gamma notation

Definition

Write $N_{0} = {0, 1, 2, \dots}$ . For $m \in N_{0}$ and $T \in R$ , define the finite-integral extension $F_{m} (T) = \int_{0}^{1} t^{2 m} \exp (- T t^{2}) d t .$ The Boys function is the restriction to the conventional domain $T \geq 0$ . The extension to negative $T$ is used only for ordinary center derivatives at the boundary value $T = 0$ . For $s > 0$ and $T > 0$ , write the lower incomplete-gamma integral as $γ (s, T) = \int_{0}^{T} u^{s - 1} \exp (- u) d u .$ The complete Euler Gamma function $Γ (s)$ has the existing meaning in Euler's Gamma function on the right half-plane, namely $Γ (s) = \int_{0}^{\infty} u^{s - 1} e^{- u} d u$ for real $s > 0$ .

The integrand defining $F_{m}$ is continuous on $[0, 1]$ and positive on $(0, 1]$ , so $F_{m} (T)$ exists, is positive, and, for $T \geq 0$ , satisfies $F_{m} (T) \leq 1 / (2 m + 1)$ . The index $m$ is an arbitrary nonnegative integer; no fixed maximum order is part of this definition.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Finite tensor contractions and their variational energy and gradient

Definition

Let $n, r \geq 1$ be integers, $C \in R^{n \times r}$ , $D \in R^{r \times r}$ , $H \in R^{n \times n}$ , and $G \in R^{n \times n \times n \times n}$ . Define their transformed tensors by $H_{p q}^{'} = \sum_{a, b = 1}^{n} C_{a p} H_{a b} C_{b q}, G_{p q r s}^{'} = \sum_{a, b, c, d = 1}^{n} C_{a p} C_{b q} C_{c r} C_{d s} G_{a b c d},$ for $1 \leq p, q, r, s \leq r$ . Define the finite variational energy functional $E (C; D, H, G) = \sum_{p, q = 1}^{r} D_{p q} H_{p q}^{'} + \frac{1}{2} \sum_{p, q, r, s = 1}^{r} D_{p q} D_{r s} G_{p q r s}^{'} .$ Its gradient $\nabla_{C} E$ is the ordinary Euclidean gradient with respect to the $n r$ real entries of $C$ . The basis dimension is $n$ , the contracted dimension is $r$ , and for any finite matrix or tensor $A$ , $∥ A ∥_{F} = (\sum ∣ A_{i_{1} \dots i_{k}} ∣^{2})^{1 / 2}$ , with the sum over all its entries. This is a finite algebraic functional; it assumes no Hartree–Fock, self-consistency, or minimizing-state postulate.

For perturbed integral tensors $\tilde{H}, \tilde{G}$ , write $\tilde{E}$ for the same functional with those tensors and the same fixed $C, D$ . The word “variational” here names the finite coefficient functional only; no claim about a stationary point or physical energy is included.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Gaussian product theorem and finite polynomial shifts

Statement

Let $a, b > 0$ , $A, B \in R^{3}$ , $p = a + b$ , $μ = a b / p$ , and $P = (a A + b B) / p$ . Then for every $x \in R^{3}$ , $\exp (- a ∥ x - A ∥_{2}^{2}) \exp (- b ∥ x - B ∥_{2}^{2}) = \exp (- μ ∥ A - B ∥_{2}^{2}) \exp (- p ∥ x - P ∥_{2}^{2}) .$ For any multi-indices $α, β \in N_{0}^{3}$ , the polynomial factor $(x - A)^{α} (x - B)^{β}$ is a finite polynomial in $x - P$ of total degree at most $∣ α ∣ + ∣ β ∣$ . Moreover, $P = (a / p) A + (b / p) B$ lies on the closed segment from $A$ to $B$ .

Facts & Assumptions

Given: $a, b > 0$ , centers $A, B \in R^{3}$ , and multi-indices $α, β \in N_{0}^{3}$ as in Cartesian Gaussian primitives, contractions, and integral conventions.

[F1]

Cartesian Gaussian primitives, contractions, and integral conventions: a primitive has exponential factor $\exp (- a ∥ x - A ∥_{2}^{2})$ and polynomial factor $(x - A)^{α}$ .

Proof

1.1givenF1algebra

Since $p = a + b > 0$ , expand the left exponent using $∥ x - A ∥^{2} = ∥ x ∥^{2} - 2 A \cdot x + ∥ A ∥^{2}$ . The quadratic and linear terms agree with $p ∥ x - P ∥^{2}$ because $p P = a A + b B$ . The remaining constant satisfies $a ∥ A ∥^{2} + b ∥ B ∥^{2} - p ∥ P ∥^{2} = \frac{a b}{p} ∥ A - B ∥^{2} = μ ∥ A - B ∥^{2},$ by substituting $P = (a A + b B) / p$ and expanding the inner products. Thus $a ∥ x - A ∥^{2} + b ∥ x - B ∥^{2} = p ∥ x - P ∥^{2} + μ ∥ A - B ∥^{2}$ , which gives the exponential identity.

1.2givenF1algebra

Each coordinate obeys $x_{j} - A_{j} = (x_{j} - P_{j}) + (P_{j} - A_{j})$ and $x_{j} - B_{j} = (x_{j} - P_{j}) + (P_{j} - B_{j})$ . The finite binomial theorem expands each integer power as a polynomial in $x_{j} - P_{j}$ of no larger degree; multiplying the six coordinate polynomials gives a finite polynomial of total degree at most $∣ α ∣ + ∣ β ∣$ .

2.1givenalgebra∎

The coefficients $a / p$ and $b / p$ are positive and sum to one. Hence $P$ is a convex combination of $A$ and $B$ , so it lies on their closed line segment, including the case $A = B$ .

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passOpen item page →

Boys integral, power series, recurrence, and incomplete-gamma representation

Statement

For every $m \in N_{0}$ and real $T$ , the extension in Boys functions and lower incomplete-gamma notation satisfies $0 < F_{m} (T) \leq \frac{1}{2 m + 1}, F_{m} (0) = \frac{1}{2 m + 1},$ $F_{m} (T) = \sum_{k = 0}^{\infty} \frac{(- T)^{k}}{k! (2 m + 2 k + 1)}, \frac{d}{d T} F_{m} (T) = - F_{m + 1} (T) .$ The upper bound in the first display is asserted for $T \geq 0$ . For $T > 0$ the function also satisfies $2 T F_{m + 1} (T) = (2 m + 1) F_{m} (T) - e^{- T}, F_{m} (T) = \frac{γ (m + \frac{1}{2}, T)}{2 T^{m + 1 / 2}} .$ The complete Gamma factor at a half-integer is $Γ (m + \frac{1}{2}) = \frac{(2 m)!}{4^{m} m!} \sqrt{π} .$

Facts & Assumptions

Given: An integer $m \geq 0$ , real $T$ , and the integral definitions of $F_{m}$ and $γ$ from Boys functions and lower incomplete-gamma notation.

[F1]

Boys functions and lower incomplete-gamma notation: $F_{m} (T) = \int_{0}^{1} t^{2 m} e^{- T t^{2}} d t$ and $γ (s, T) = \int_{0}^{T} u^{s - 1} e^{- u} d u$ for $s, T > 0$ .

[F2]

Euler's Gamma function on the right half-plane: for real $s > 0$ , $Γ (s) = \int_{0}^{\infty} u^{s - 1} e^{- u} d u$ .

[F3]

The Gaussian integral $\int_{- \infty}^{\infty} e^{- x^{2}} d x = \sqrt{π}$ : $\int_{- \infty}^{\infty} e^{- x^{2}} d x = \sqrt{π}$ .

[F4]

The Gamma functional equation: $Γ (s + 1) = s Γ (s)$ for real $s > 0$ .

[F5]

Change of variable in an improper integral: a monotone differentiable surjection between intervals preserves convergent improper integrals when its derivative and the target integrand are locally Riemann integrable and the proper change-of-variable hypotheses hold on every compact truncation. Each singular end is treated separately.

[F6]

If $u, v$ are differentiable on $[a, b]$ with $u^{'}, v^{'}$ integrable, then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ : on a compact interval, $\int u v^{'} = u v ∣_{\partial} - \int u^{'} v$ when the stated integrability hypotheses hold.

[F7]

Dominated convergence: pointwise limits may pass through a Lebesgue integral when one integrable majorant bounds the sequence almost everywhere.

[F8]

Mean value theorem on a closed real interval: a scalar difference quotient equals a derivative value at an intermediate point of the parameter interval.

[F9]

The real exponential function and the number $e$ by a power series: $\exp (x) = \sum_{k = 0}^{\infty} x^{k} / k!$ for real $x$ , with convergence for every $x$ .

[L9]

The exponential function is smooth and $(\exp)^{'} = \exp$ and Sum, product, quotient, and chain rules from difference quotients: the exponential is smooth with derivative itself; finite sums, products and polynomial compositions obey the product, power and chain rules. Applying these rules one coordinate or parameter at a time justifies every displayed finite Gaussian derivative.

Proof

1.1givenF1F7F8F9algebraL9

The integrand in [F1] is positive for every real $T$ ; when $T \geq 0$ it is at most $t^{2 m}$ , whose integral is $1 / (2 m + 1)$ . Setting $T = 0$ gives equality. By [F9], on a compact parameter interval $[- M, M]$ the exponential-series partial sums converge pointwise on $[0, 1]$ and are bounded in absolute value by $e^{M}$ ; [F7] therefore permits integration term by term and gives the displayed series. For a fixed $T$ , choose $M > ∣ T ∣ + 1$ and $∣ h ∣ < 1$ . By [F8] and the chain rule, the difference quotient of $e^{- T t^{2}}$ in $T$ is $- t^{2} e^{- ξ t^{2}}$ for some $ξ$ between $T$ and $T + h$ , so after multiplication by $t^{2 m}$ it is bounded by $e^{M} t^{2 m + 2}$ . Dominated convergence [F7] passes the difference-quotient limit through the integral and gives $F_{m}^{'} (T) = - F_{m + 1} (T)$ .

1.2givenF1F6algebra

On $[0, 1]$ , integrate by parts [F6] with $u (t) = t^{2 m + 1}$ and $v^{'} (t) = - 2 T t e^{- T t^{2}}$ , so $v (t) = e^{- T t^{2}}$ . The boundary increment is $e^{- T}$ , while the two integrals are $- 2 T F_{m + 1} (T)$ and $- (2 m + 1) F_{m} (T)$ . Rearranging gives $2 T F_{m + 1} = (2 m + 1) F_{m} - e^{- T}$ .

1.3givenF1F5algebra

For $T > 0$ , use the increasing surjection $t = \sqrt{u / T}$ from $(0, T]$ to $(0, 1]$ . Its derivative is continuous on compact truncations away from zero, as are the integrands, so the proper substitution hypotheses of [F5] hold there. Then $d t = \frac{1}{2} T^{- 1 / 2} u^{- 1 / 2} d u$ and $t^{2 m} = T^{- m} u^{m}$ , giving $γ (m + \frac{1}{2}, T) / (2 T^{m + 1 / 2})$ on passage to the zero endpoint. The original integrand is bounded there, and the transformed one is bounded by a constant times $u^{m - 1 / 2}$ , whose exponent is greater than $- 1$ ; both improper integrals therefore converge.

2.1givenF2F3F4F5algebra∎

In [F2], substitute $u = x^{2}$ for $Γ (1 / 2)$ . This is an increasing differentiable surjection of $(0, \infty)$ onto itself, with continuous derivative and continuous integrands on compact truncations away from zero; hence [F5] applies separately at zero and infinity. The transformed integrand is $2 e^{- x^{2}}$ , integrable at both ends by [F3], so symmetry gives $Γ (1 / 2) = 2 \int_{0}^{\infty} e^{- x^{2}} d x = \sqrt{π}$ . Repeated use of [F4] gives $Γ (m + \frac{1}{2}) = \prod_{j = 0}^{m - 1} (j + \frac{1}{2}) \sqrt{π}$ . Multiplying the odd factors yields $(2 m)! / (4^{m} m!)$ , proving the half-integer formula, including the empty product when $m = 0$ .

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passOpen item page →

A positive midpoint enclosure for Boys functions on bounded arguments

Statement

For $m \in N_{0}$ , $T \geq 0$ , and integer $N \geq 1$ , let $h = 1 / N$ , $t_{j} = (j - \frac{1}{2}) h$ for $1 \leq j \leq N$ , and $Q_{m, N} (T) = h \sum_{j = 1}^{N} t_{j}^{2 m} e^{- T t_{j}^{2}} .$ Then all quadrature weights and summands are positive and $∣ F_{m} (T) - Q_{m, N} (T) ∣ \leq \frac{m + T}{2 N} .$ Consequently, for $0 \leq T \leq T_{\max}$ , the same positive rule has the uniform enclosure error $(m + T_{\max}) / (2 N)$ .

Facts & Assumptions

Given: $F_{m} (T)$ as in Boys functions and lower incomplete-gamma notation, $m \geq 0$ , $T \geq 0$ , and $N \geq 1$ .

[F1]

Boys functions and lower incomplete-gamma notation: $F_{m} (T) = \int_{0}^{1} f (t) d t$ with $f (t) = t^{2 m} e^{- T t^{2}}$ .

[F2]

Mean value theorem on a closed real interval: a differentiable function whose derivative has absolute value at most $L$ varies by at most $L$ times the distance between two points.

[L9]

Proof

1.1givenF1F2algebraL9

For $m = 0$ , $f^{'} (t) = - 2 T t e^{- T t^{2}}$ , so $∣ f^{'} (t) ∣ \leq 2 T$ . For $m \geq 1$ , differentiation gives $f^{'} (t) = 2 m t^{2 m - 1} e^{- T t^{2}} - 2 T t^{2 m + 1} e^{- T t^{2}}$ ; since $0 \leq t \leq 1$ and $e^{- T t^{2}} \leq 1$ , $∣ f^{'} (t) ∣ \leq 2 m + 2 T$ . Thus the Lipschitz constant $L = 2 m + 2 T$ is valid in both cases by [F2].

2.1givenstep 1.1algebra

On each subinterval of length $h$ , the mean-value bound gives $∣ f (t) - f (t_{j}) ∣ \leq L ∣ t - t_{j} ∣$ . Integrating over that subinterval yields error at most $L h^{2} / 4$ , because the integral of distance from its midpoint is $h^{2} / 4$ . Summing $N$ subintervals gives $L / (4 N) = (m + T) / (2 N)$ . All midpoints and weights are positive and $f (t_{j}) > 0$ .

3.1givenstep 2.1algebra∎

If $T \leq T_{\max}$ , then $(m + T) / (2 N) \leq (m + T_{\max}) / (2 N)$ ; hence the stated uniform bound follows without changing the positive weights or nodes.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passOpen item page →

Cartesian Gaussian moments and exponent-parameter derivatives

Statement

Let $p > 0$ and $α \in N_{0}^{3}$ . If any component of $α$ is odd, then $\int_{R^{3}} x^{α} e^{- p ∥ x ∥_{2}^{2}} d x = 0.$ If $α_{j} = 2 k_{j}$ for $j = 1, 2, 3$ , then $\int_{R^{3}} x^{α} e^{- p ∥ x ∥_{2}^{2}} d x = π^{3 / 2} \prod_{j = 1}^{3} \frac{(2 k_{j})!}{4^{k_{j}} k_{j}! p^{k_{j} + 1 / 2}} .$ For every $q \in N_{0}$ , differentiation with respect to $p$ is valid and $\frac{d^{q}}{d p^{q}} \int_{R^{3}} x^{α} e^{- p ∥ x ∥_{2}^{2}} d x = (- 1)^{q} \int_{R^{3}} ∥ x ∥_{2}^{2 q} x^{α} e^{- p ∥ x ∥_{2}^{2}} d x .$

Facts & Assumptions

Given: $p > 0$ , a multi-index $α \in N_{0}^{3}$ , and the Lebesgue integral convention of Cartesian Gaussian primitives, contractions, and integral conventions.

[F1]

The Gaussian integral $\int_{- \infty}^{\infty} e^{- x^{2}} d x = \sqrt{π}$ : $\int_{R} e^{- x^{2}} d x = \sqrt{π}$ .

[F2]

If $u, v$ are differentiable on $[a, b]$ with $u^{'}, v^{'}$ integrable, then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ : finite-interval integration by parts holds when the displayed functions and derivatives are integrable.

[F3]

Tonelli's theorem for nonnegative measurable functions on a sigma-finite product: nonnegative measurable functions on a sigma-finite product may be integrated by sections in either order.

[F4]

Fubini's theorem for L^1 functions on a sigma-finite product: absolutely integrable functions on a sigma-finite product have equal iterated and product integrals.

[F5]

Dominated convergence: pointwise convergence under a single integrable majorant permits passage of the limit through the integral.

[F6]

Mean value theorem on a closed real interval: a difference quotient of a differentiable scalar function is bounded by the supremum of its derivative on the intervening segment.

[F7]

[L9]

[F8]

The real exponential function and the number $e$ by a power series: $e^{x}$ is given by its convergent power series for real $x$ .

Proof

1.1givenF1F2F7F8algebraL9

For each integer $d \geq 0$ , $∣ x ∣^{d} e^{- p x^{2}}$ is absolutely integrable. If $d > 0$ , differentiating $r^{d} e^{- p r^{2} / 2}$ shows it increases up to $r = \sqrt{d / p}$ and decreases afterwards, so it is bounded by $(d / p)^{d / 2}$ ; for $d = 0$ it is bounded by $1$ . Thus $∣ x ∣^{d} e^{- p x^{2}} \leq C_{d} e^{- p x^{2} / 2}$ for a finite $C_{d}$ , whose right-hand side is integrable by scaling and [F1], [F7]. Write $J_{k} (p) = \int_{R} x^{2 k} e^{- p x^{2}} d x$ for $k \geq 0$ . Then $J_{0} (p) = \sqrt{π} p^{- 1 / 2}$ by scaling $y = \sqrt{p} x$ and [F1], [F7], and odd moments vanish by $x \mapsto - x$ , now with absolute convergence established. All these scaling and reflection maps are linear surjections with continuous derivatives; the integrands are continuous on every compact truncation, so [F7] applies separately at both infinite ends. Fix $k \geq 1$ for the moment recurrence below. For its boundary term choose an integer $N > (2 k - 1) / 2$ . By [F8] and $e^{- p R^{2} / 2} \leq 1$ , $R^{2 k - 1} e^{- p R^{2}} \leq N! (2 / p)^{N} R^{2 k - 1 - 2 N} ⟶ 0.$ Integration by parts [F2] on $[- R, R]$ with $d v = x e^{- p x^{2}} d x = - d (e^{- p x^{2}}) / (2 p)$ therefore gives $J_{k} (p) = (2 k - 1) J_{k - 1} (p) / (2 p)$ after $R \to \infty$ . Iterating yields $J_{k} (p) = \sqrt{π} (2 k)! / (4^{k} k! p^{k + 1 / 2})$ .

2.1givenF3F4step 1.1algebra

The absolute value of each three-dimensional integrand is a product of three one-dimensional polynomial-Gaussian factors. Their integrals are finite by step 1.1, so [F3] and then [F4] factor the integral into the product of the three one-dimensional moments. If a component is odd, its factor is zero; otherwise multiplying the three formulas from step 1.1 gives the displayed expression.

3.1givenF5F6step 1.1step 2.1inductionL9∎

Fix $p_{0} > 0$ and restrict $p$ to $[p_{0} / 2, 3 p_{0} / 2]$ . The absolute value of each $q$ -th parameter derivative integrand is bounded by $∥ x ∥^{∣ α ∣ + 2 q} e^{- (p_{0} / 2) ∥ x ∥^{2}}$ . This is integrable by step 2.1: bound $∥ x ∥^{d} \leq (∣ x_{1} ∣ + ∣ x_{2} ∣ + ∣ x_{3} ∣)^{d}$ , expand the finite power, and use the absolute one-dimensional moments established in step 1.1. Difference quotients for one derivative are bounded by the corresponding next polynomial-Gaussian majorant by [F6]; [F5] therefore passes each limit through the integral. Repeating this argument $q$ times gives the stated factor $(- 1)^{q} ∥ x ∥^{2 q}$ .

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Explicit finite-dimensional contraction error bounds for energy and gradient

Statement

Let $n, r \geq 1$ , $C \in R^{n \times r}$ with $∥ C ∥_{F} \leq B$ , and $D \in R^{r \times r}$ with $∥ D ∥_{F} \leq M$ . Suppose $∣ {\tilde{H}}_{a b} - H_{a b} ∣ \leq ε_{2}$ and $∣ {\tilde{G}}_{a b c d} - G_{a b c d} ∣ \leq ε_{4}$ for every entry. With the functional of Finite tensor contractions and their variational energy and gradient, $∣ \tilde{E} - E ∣ \leq M r n B^{2} ε_{2} + \frac{1}{2} M^{2} r^{2} n^{2} B^{4} ε_{4},$ and $∥ \nabla_{C} \tilde{E} - \nabla_{C} E ∥_{F} \leq 2 n r B M ε_{2} + 2 n^{2} r^{2} B^{3} M^{2} ε_{4} .$

Facts & Assumptions

Given: The finite real functional in Finite tensor contractions and their variational energy and gradient, dimensions $n, r \geq 1$ , and the entrywise error bounds and norm bounds in the statement.

[F1]

Finite tensor contractions and their variational energy and gradient: $H^{'}$ has two factors of $C$ , $G^{'}$ has four, $E = ⟨ D, H^{'} ⟩_{F} + \frac{1}{2} \sum D_{p q} D_{r s} G_{p q r s}^{'}$ , and the gradient is with respect to the $n r$ entries of $C$ .

[F2]

Cauchy-Schwarz inequality for $L^{2}$ : on a finite counting measure, $∥ x ∥_{1} \leq \sqrt{k} ∥ x ∥_{2}$ for a vector with $k$ entries.

Proof

1.1givenF1F2algebra

Apply [F2] to each column $c_{p}$ of $C$ : $∥ c_{p} ∥_{1} \leq \sqrt{n} ∥ c_{p} ∥_{2} \leq \sqrt{n} B$ . Therefore every transformed one-body error satisfies $∣ Δ H_{p q}^{'} ∣ \leq ε_{2} ∥ c_{p} ∥_{1} ∥ c_{q} ∥_{1} \leq n B^{2} ε_{2}$ . With $r^{2}$ entries, $∥ Δ H^{'} ∥_{F} \leq r n B^{2} ε_{2}$ .

1.2givenF1F2algebra

Each transformed four-index error is bounded by $ε_{4} \prod_{j \in {p, q, r, s}} ∥ c_{j} ∥_{1} \leq n^{2} B^{4} ε_{4}$ . There are $r^{4}$ entries, so $∥ Δ G^{'} ∥_{F} \leq r^{2} n^{2} B^{4} ε_{4}$ . The rank-two coefficient tensor $(D_{p q} D_{r s})$ has Frobenius norm $∥ D ∥_{F}^{2} \leq M^{2}$ .

1.3givenF1F2algebra

For a fixed entry $C_{a μ}$ , differentiating the two occurrences of $C$ in $H^{'}$ yields two sums. Each row of $D$ or column of $D$ has $ℓ^{1}$ norm at most $\sqrt{r} M$ by [F2], while $\sum_{b} ∣ Δ H_{a b} ∣ ∣ C_{b q} ∣ \leq \sqrt{n} B ε_{2}$ . Thus each gradient entry from $H$ has magnitude at most $2 \sqrt{n r} B M ε_{2}$ , and the Frobenius norm over $n r$ entries is at most $2 n r B M ε_{2}$ .

1.4givenF1F2algebra

Differentiating the four factors of $C$ in $G^{'}$ gives four sums. For each fixed slot, the sum over the other three basis indices is at most $n^{3 / 2} B^{3} ε_{4}$ by [F2]. The remaining coefficient sum over the three orbital indices is at most $r^{3 / 2} M^{2}$ : one row or column of $D$ has $ℓ^{1}$ norm at most $\sqrt{r} M$ and all entries of the other copy sum to at most $r M$ . Including the factor $1 / 2$ and four slots, each gradient entry is bounded by $2 n^{3 / 2} r^{3 / 2} B^{3} M^{2} ε_{4}$ . Multiplying by $\sqrt{n r}$ for its $n r$ entries gives $2 n^{2} r^{2} B^{3} M^{2} ε_{4}$ .

2.1step 1.1step 1.2algebra

By finite Cauchy–Schwarz, the one-body energy error is at most $∥ D ∥_{F} ∥ Δ H^{'} ∥_{F} \leq M r n B^{2} ε_{2}$ . Pairing $(D_{p q} D_{r s})$ with $Δ G^{'}$ gives the two-body bound $\frac{1}{2} M^{2} r^{2} n^{2} B^{4} ε_{4}$ . Adding them proves the energy estimate.

3.1step 1.3step 1.4algebra∎

The full gradient error is the sum of the one-body and two-body gradient errors. The triangle inequality and steps 1.3 and 1.4 give the claimed bound.

DefinitionDefinition: AI-adaptedProof: Not applicableOpen item page →

Hermite Gaussian and Boys Coulomb auxiliary functions

Definition

Using $N_{0} = {0, 1, 2, \dots}$ from Cartesian Gaussian primitives, contractions, and integral conventions, for $p > 0$ , $P \in R^{3}$ , and $t, u, v \in N_{0}$ , the Hermite Gaussian is $Λ_{t u v} (x; p, P) = \frac{\partial^{t + u + v}}{\partial P_{1}^{t} \partial P_{2}^{u} \partial P_{3}^{v}} \exp (- p ∥ x - P ∥_{2}^{2}) .$ For $η > 0$ , $P, C \in R^{3}$ , and $n, t, u, v \in N_{0}$ , define the Boys Coulomb auxiliary function $R_{t u v}^{n} (η, P - C) = (- 2 η)^{n} \frac{\partial^{t + u + v}}{\partial P_{1}^{t} \partial P_{2}^{u} \partial P_{3}^{v}} F_{n} ⁣ (η ∥ P - C ∥_{2}^{2}) .$ Each derivative is an ordinary derivative of a smooth real function of the displayed center coordinates. For the Gaussian this follows from The exponential function is smooth and $(\exp)^{'} = \exp$ and repeated coordinatewise product and chain rules in Sum, product, quotient, and chain rules from difference quotients. For the Boys composition, Boys integral, power series, recurrence, and incomplete-gamma representation gives $F_{n}^{(k)} (T) = (- 1)^{k} F_{n + k} (T)$ by iteration on the full real extension; these derivatives are continuous by its integral representation and compact-uniform domination. The chain rules therefore also apply when $P = C$ , where the Boys argument is zero. The multi-index $(t, u, v)$ records derivative order and $n$ records Boys order; both are nonnegative integers.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passOpen item page →

Absolute convergence and local parameter domination for Gaussian basis integrals

Statement

Every overlap, kinetic, point-nucleus attraction, and two-electron Coulomb integral defined in Cartesian Gaussian primitives, contractions, and integral conventions exists absolutely for finite Cartesian Gaussian contractions. The same holds when Gaussian factors are replaced by any fixed finite spatial derivatives, also after any fixed finite number of derivatives with respect to primitive centers or positive exponents. The Coulomb kernels are left undifferentiated; arbitrary spatial derivatives of the whole singular integrand are not asserted to be absolutely integrable. With nuclear positions fixed, if primitive centers remain in compact sets and all exponents remain in a compact subset of $(0, \infty)$ , these differentiated integrands have a common integrable majorant for each fixed derivative order. Thus differentiation with respect to primitive centers or exponents may be passed under any of these integrals to every finite order.

Facts & Assumptions

Given: Finite contractions as in Cartesian Gaussian primitives, contractions, and integral conventions, with positive exponents, fixed finite polynomial degrees, and (for the local domination assertion) centers and exponents in the compact parameter sets of the Statement.

[F1]

Cartesian Gaussian primitives, contractions, and integral conventions: each primitive is a polynomial times $e^{- a ∥ x - A ∥^{2}}$ , and the Coulomb kernels are $∥ x - C ∥^{- 1}$ and $∥ x - y ∥^{- 1}$ .

[F2]

Cartesian Gaussian moments and exponent-parameter derivatives: every polynomial times $e^{- p ∥ x ∥^{2}}$ is absolutely integrable for $p > 0$ .

[F3]

Tonelli's theorem for nonnegative measurable functions on a sigma-finite product: nonnegative integrands may be estimated by iterated integrals.

[F4]

Fubini's theorem for L^1 functions on a sigma-finite product: an absolutely integrable complex integrand has a well-defined product integral and equal iterated integrals.

[F5]

Dominated convergence: a common integrable majorant permits passage of a pointwise parameter-derivative limit through an integral.

[L8]

Mean value theorem on a closed real interval: a scalar difference quotient is bounded by the supremum of the derivative on its parameter segment.

[L9]

Proof

1.1givenF1F2algebraL9

Repeated product-rule differentiation shows that every fixed spatial or primitive-parameter derivative of a Gaussian factor is a finite sum of polynomial-Gaussian terms. On the compact parameter sets in the Statement, choose $0 < a_{0} \leq a \leq a_{1} < \infty$ and $∥ A ∥ \leq R$ . The coefficients of these finitely many polynomials are bounded uniformly, since they are polynomials in the bounded parameters. Moreover, $∥ x - A ∥^{2} \geq \frac{1}{2} ∥ x ∥^{2} - ∥ A ∥^{2}$ and $e^{- a ∥ x - A ∥^{2}} \leq e^{- a_{0} ∥ x - A ∥^{2}} \leq e^{a_{0} R^{2}} e^{- a_{0} ∥ x ∥^{2} / 2}$ . Each term is therefore bounded by $K (1 + ∥ x ∥)^{N} e^{- a_{0} ∥ x ∥^{2} / 2}$ for finite $K, N$ uniform on those parameter sets. This majorant is integrable by [F2] and bounded, so each pair product is in $L^{1} \cap L^{\infty}$ ; products involving $Δ ψ$ have the same form. For fixed parameters use singleton compact sets.

2.1givenF1F3step 1.1algebra

The overlap and kinetic integrands are polynomial-Gaussian products and are absolutely integrable by step 1.1. For a nuclear center $C$ , the pair product is bounded on $∥ x - C ∥ < 1$ . To check local kernel integrability without a radial-coordinate formula, partition $0 < ∥ z ∥ < 1$ into $A_{k} = {2^{- (k + 1)} \leq ∥ z ∥ < 2^{- k}}$ : on $A_{k}$ , $∥ z ∥^{- 1} \leq 2^{k + 1}$ and $A_{k}$ lies in a cube of volume $8 \cdot 2^{- 3 k}$ , so $\int_{A_{k}} ∥ z ∥^{- 1} d z \leq 16 \cdot 4^{- k}$ . The sum is $64 / 3$ . Outside this unit ball the kernel is at most one, so the remaining integral is bounded by the pair product's $L^{1}$ norm. This proves absolute convergence of the point-nucleus attraction.

3.1givenF1F3F4step 1.1step 2.1algebra

Let $f, g$ be two pair products from finite contractions; by step 1.1 they belong to $L^{1} \cap L^{\infty}$ . On $∥ x - y ∥ < 1$ , Tonelli [F3] and $z = y - x$ give the bound $∥ f ∥_{1} ∥ g ∥_{\infty} \int_{∥ z ∥ < 1} ∥ z ∥^{- 1} d z \leq (64 / 3) ∥ f ∥_{1} ∥ g ∥_{\infty}$ by the shell calculation in step 2.1. On the complement, $∥ x - y ∥^{- 1} \leq 1$ , giving bound $∥ f ∥_{1} ∥ g ∥_{1}$ . Hence the two-electron integrand is absolutely integrable, and [F4] supplies its product and iterated integral meanings.

4.1givenF1F3F5L8step 1.1step 2.1step 3.1algebraL9∎

All the allowed derivatives act on Gaussian factors, so at every fixed finite order step 1.1 applies; the kernels, singular centers $C$ , and diagonal $x = y$ remain fixed. Products of those uniform Gaussian envelopes, multiplied by the unchanged kernel when present, are common integrable majorants by steps 2.1 and 3.1. For difference quotients, enlarge the compact parameter bounds slightly within the positive-exponent domain so they contain all sufficiently short parameter segments. Apply [L8] to each real Gaussian term on such a segment; its quotient is bounded by the envelope for the corresponding next derivative. The same near-nucleus and near-diagonal estimates make these quotient bounds integrable. Applying [F5] passes the derivative through the integral; repeating at each fixed finite order proves the mixed-derivative assertion. Fixed complex coefficients and finite contraction sums are handled by finite linearity and the triangle inequality.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passOpen item page →

A monotone-range Taylor remainder for small Boys arguments

Statement

Let $m, N \in N_{0}$ , $T \geq 0$ , and $N + 2 \geq T$ . Then $∣ F_{m} (T) - \sum_{k = 0}^{N} \frac{(- T)^{k}}{k! (2 m + 2 k + 1)} ∣ \leq \frac{T^{N + 1}}{(N + 1)! (2 m + 2 N + 3)} .$ In particular, this is a valid finite Taylor certificate whenever $0 \leq T \leq 1$ .

Facts & Assumptions

Given: $F_{m}$ and its absolutely convergent series as in Boys functions and lower incomplete-gamma notation and Boys integral, power series, recurrence, and incomplete-gamma representation, with $m, N \geq 0$ , $T \geq 0$ , and $N + 2 \geq T$ .

[F1]

Boys integral, power series, recurrence, and incomplete-gamma representation: $F_{m} (T) = \sum_{k \geq 0} (- T)^{k} / [k! (2 m + 2 k + 1)]$ .

Proof

1.1givenF1algebra

Set $a_{k} = T^{k} / [k! (2 m + 2 k + 1)]$ . For $T > 0$ , $\frac{a_{k + 1}}{a_{k}} = \frac{T}{k + 1} \frac{2 m + 2 k + 1}{2 m + 2 k + 3} \leq \frac{T}{k + 1} .$ For every $k \geq N + 1$ , $k + 1 \geq N + 2 \geq T$ , and the second factor is strictly less than one, so the positive terms decrease from the first omitted term onward.

2.1givenF1step 1.1algebra∎

The tail in [F1] after term $N$ is alternating with decreasing positive magnitudes by step 1.1; pairing consecutive terms shows its absolute value is at most $a_{N + 1}$ . That value is the displayed bound. If $T = 0$ , the tail and bound are both zero.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passOpen item page →

A scaled incomplete-gamma tail bound for large Boys arguments

Statement

Let $m \in N_{0}$ , $s = m + \frac{1}{2}$ , and $T > \max {s - 1, 0}$ . Then $F_{m} (T) = \frac{Γ (s) - R_{s} (T)}{2 T^{s}}, R_{s} (T) = \int_{T}^{\infty} u^{s - 1} e^{- u} d u,$ and $0 \leq R_{s} (T) \leq \frac{T^{s - 1} e^{- T}}{1 - \max {s - 1, 0} / T} .$ Consequently a certified enclosure of $Γ (s)$ and $e^{- T}$ gives the interval $[\frac{Γ (s)}{2 T^{s}} - \frac{T^{s - 1} e^{- T}}{2 T^{s} (1 - \max {s - 1, 0} / T)}, \frac{Γ (s)}{2 T^{s}}]$ after intersecting its lower endpoint with zero. In the evaluator's large branch $T > 2 m + 1$ , the denominator is at least $1 / 2$ .

Facts & Assumptions

Given: $m \geq 0$ , $s = m + 1 / 2$ , $T > \max {s - 1, 0}$ , and the definitions in Boys functions and lower incomplete-gamma notation and Euler's Gamma function on the right half-plane.

[F1]

Boys integral, power series, recurrence, and incomplete-gamma representation: $F_{m} (T) = γ (s, T) / (2 T^{s})$ .

[F2]

Euler's Gamma function on the right half-plane: $Γ (s) = \int_{0}^{\infty} u^{s - 1} e^{- u} d u$ for $s > 0$ .

[F3]

Additivity of the nonnegative Lebesgue integral: splitting a nonnegative integral over adjacent intervals adds the two integrals.

Proof

1.1givenF1F2F3algebra

By [F2]–[F3], $Γ (s) = γ (s, T) + R_{s} (T)$ , so [F1] gives the scaled identity. The tail is nonnegative.

1.2givenalgebra

Substitute $u = T + v$ into $R_{s} (T)$ . If $s \geq 1$ , then $(T + v)^{s - 1} = T^{s - 1} (1 + v / T)^{s - 1} \leq T^{s - 1} e^{(s - 1) v / T}$ because $1 + w \leq e^{w}$ for $w \geq 0$ . Hence $R_{s} (T) \leq T^{s - 1} e^{- T} \int_{0}^{\infty} e^{- (1 - (s - 1) / T) v} d v$ , whose integral is $1 / (1 - (s - 1) / T)$ . If $0 < s < 1$ , then $(T + v)^{s - 1} \leq T^{s - 1}$ , yielding $R_{s} (T) \leq T^{s - 1} e^{- T}$ . These are the combined bound.

2.1givenstep 1.1step 1.2algebra∎

For $s = m + 1 / 2$ , $\max {s - 1, 0} \leq m$ ; if $T > 2 m + 1$ , then $\max {s - 1, 0} / T < 1 / 2$ . Substitution into step 1.2 gives the evaluator's large-branch denominator bound and the interval enclosure.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passOpen item page →

Upward and downward Boys recurrence error amplification bounds

Statement

Let $m \geq 0$ , $T > 0$ , and let $I_{m} = [c_{m} - r_{m}, c_{m} + r_{m}]$ enclose $F_{m} (T)$ while $J = [c_{e} - r_{e}, c_{e} + r_{e}]$ encloses $e^{- T}$ . The exact upward recurrence image for $F_{m + 1}$ has radius at most $\frac{(2 m + 1) r_{m} + r_{e}}{2 T},$ and the exact downward recurrence image for $F_{m}$ , from an interval of radius $r_{m + 1}$ for $F_{m + 1}$ , has radius at most $\frac{2 T r_{m + 1} + r_{e}}{2 m + 1} .$ If each full affine image is formed exactly before its two endpoints are converted outward once, and both conversions are finite, the stored interval radius exceeds the exact-image radius by the mean of the two endpoint-rounding errors. Iterating the displayed bounds with these rounding contributions gives valid finite error-amplification estimates over any requested order range for which every conversion is finite. An implementation rounding at intermediate primitive nodes must also propagate those nodes' rounding contributions; the final two conversion errors alone do not bound its total widening. If any required conversion overflows, no finite recurrence interval or finite propagated estimate is asserted for that step. Upward recurrence is undefined at $T = 0$ ; direct values $F_{m} (0) = 1 / (2 m + 1)$ are exact.

Facts & Assumptions

Given: The recurrence identity in Boys integral, power series, recurrence, and incomplete-gamma representation, enclosing intervals $I_{m}, J$ , and the outward interval operations in Outward-rounded interval, rectangle and ball operations.

[F1]

Boys integral, power series, recurrence, and incomplete-gamma representation: $F_{m + 1} = ((2 m + 1) F_{m} - e^{- T}) / (2 T)$ for $T > 0$ , and equivalently $F_{m} = (2 T F_{m + 1} + e^{- T}) / (2 m + 1)$ .

[F2]

Outward-rounded interval, rectangle and ball operations: each primitive interval operation forms its specified exact endpoint formulas and then rounds outward. A composition of these operations can round at intermediate nodes; this does not prescribe a single conversion of the full affine recurrence image.

[F3]

Outward-rounded operations are inclusion-isotone and enclose DAG evaluations: finite outward interval expression graphs enclose their exact values.

[F4]

Directed dyadic rounding encloses with explicit underflow and overflow bounds: for an exact endpoint within the finite format range, directed rounding is outward with the stated finite error bound. Overflow has error bound $+ \infty$ , even when one directed rounding saturates at a finite extremal endpoint; the enclosing pair then includes an infinite endpoint.

Proof

1.1givenF1algebra

The exact upward map is affine with positive coefficient $(2 m + 1) / (2 T)$ on $F_{m}$ and coefficient $- 1 / (2 T)$ on $e^{- T}$ . Therefore the radius of its exact interval image is at most $((2 m + 1) r_{m} + r_{e}) / (2 T)$ . The downward map has positive coefficients $2 T / (2 m + 1)$ and $1 / (2 m + 1)$ , so its exact interval image radius is at most $(2 T r_{m + 1} + r_{e}) / (2 m + 1)$ .

2.1givenF2F4step 1.1algebra

Under the stated single-conversion prescription, let $[L, U]$ be the exact full affine image. By [F4], its stored endpoints are $L - δ_{-}$ and $U + δ_{+}$ with $δ_{-}, δ_{+} \geq 0$ . Its radius is exactly $(U - L) / 2 + (δ_{-} + δ_{+}) / 2$ . This follows from directed conversion of the full endpoints, not from identifying a composition of [F2]'s primitive operations with one rounding. If either conversion overflows, [F4] supplies no finite error bound and no finite-radius claim is made.

3.1F2F3F4step 2.1algebra

If rounding occurs at intermediate affine nodes, apply the same radius calculation at each node. For a node forming $a X + b Y + d$ with exact real scalars $a, b, d$ , input radii $r_{X}, r_{Y}$ , and mean outward endpoint error $h$ , its stored radius is $∣ a ∣ r_{X} + ∣ b ∣ r_{Y} + h$ . Consequently each intermediate contribution is carried through subsequent absolute affine coefficients, in addition to the final node's contribution. More generally [F3] ensures containment through the actual primitive graph, but gives no bound on total widening using only the last two rounding errors.

4.1givenF1F4step 1.1step 2.1step 3.1algebra∎

The recurrence identities in [F1] show that each exact target value belongs to its exact interval image, and outward conversion preserves this inclusion. For full affine images with one conversion per endpoint, applying steps 1.1 and 2.1 successively yields the stated finite propagated bounds. Step 3.1 accounts for intermediate rounding when present. At $T = 0$ , [F1] gives $F_{m} (0) = 1 / (2 m + 1)$ , while the upward formula divides by zero and is excluded.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Finite Hermite expansion and coefficient recurrences for a Cartesian Gaussian pair

Statement

In one dimension, let $g_{i} (x_{A}, a) = x_{A}^{i} e^{- a x_{A}^{2}}$ and $g_{j} (x_{B}, b) = x_{B}^{j} e^{- b x_{B}^{2}}$ , with $x_{A} = x - A$ , $x_{B} = x - B$ , $p = a + b$ , $P = (a A + b B) / p$ , and $K = e^{- a b (A - B)^{2} / p}$ . There are unique coefficients $E_{i j}^{t}$ such that $g_{i} (x_{A}, a) g_{j} (x_{B}, b) = \sum_{t = 0}^{i + j} E_{i j}^{t} Λ_{t} (x; p, P) .$ With $E_{00}^{0} = K$ and $E_{i j}^{t} = 0$ outside $0 \leq t \leq i + j$ , they satisfy $E_{i + 1, j}^{t} = \frac{E_{i j}^{t - 1}}{2 p} + (P - A) E_{i j}^{t} + (t + 1) E_{i j}^{t + 1},$ $E_{i, j + 1}^{t} = \frac{E_{i j}^{t - 1}}{2 p} + (P - B) E_{i j}^{t} + (t + 1) E_{i j}^{t + 1} .$ In three dimensions the pair expansion is the product of the three one-dimensional expansions, so it is a finite sum of $Λ_{t u v}$ with $0 \leq t \leq α_{1} + β_{1}$ , $0 \leq u \leq α_{2} + β_{2}$ , and $0 \leq v \leq α_{3} + β_{3}$ .

Facts & Assumptions

Given: Primitive Gaussian factors and indices as above, the product identity of Gaussian product theorem and finite polynomial shifts, and $Λ_{t}$ from Hermite Gaussian and Boys Coulomb auxiliary functions.

[F1]

Gaussian product theorem and finite polynomial shifts: the product exponential equals $K e^{- p (x - P)^{2}}$ and the remaining polynomial has degree at most $i + j$ .

[F2]

Hermite Gaussian and Boys Coulomb auxiliary functions: $Λ_{t} = \partial_{P}^{t} e^{- p (x - P)^{2}}$ .

[L9]

Proof

1.1givenF2algebrainductionL9

Differentiating [F2] once gives $Λ_{t + 1} = 2 p \partial_{P}^{t} ((x - P) e^{- p (x - P)^{2}})$ . The product rule applied $t$ times gives $\partial_{P}^{t} ((x - P) h) = (x - P) \partial_{P}^{t} h - t \partial_{P}^{t - 1} h$ , hence $(x - P) Λ_{t} = \frac{Λ_{t + 1}}{2 p} + t Λ_{t - 1},$ with the last term zero for $t = 0$ .

2.1givenF1F2step 1.1algebrainduction

The polynomial factors $x_{A}^{i} x_{B}^{j}$ have degree at most $i + j$ . By [F1] they multiply a common Gaussian. The polynomial part of $Λ_{t}$ has degree $t$ and leading coefficient $(2 p)^{t}$ , as follows inductively from $Λ_{t + 1} = 2 p (x - P) Λ_{t} - 2 p t Λ_{t - 1}$ . Thus these polynomials form a triangular basis of the polynomials of degree at most $i + j$ , which gives existence and uniqueness of the finite coefficients $E_{i j}^{t}$ .

3.1step 1.1step 2.1algebra

Multiplying the expansion for $g_{i} g_{j}$ by $x_{A} = (x - P) + (P - A)$ gives the expansion for $g_{i + 1} g_{j}$ . Substitute the identity in step 1.1 and collect the coefficient of each $Λ_{t}$ ; it is $E_{i j}^{t - 1} / (2 p) + (P - A) E_{i j}^{t} + (t + 1) E_{i j}^{t + 1}$ . Replacing $x_{A}$ by $x_{B} = (x - P) + (P - B)$ proves the second recurrence. The zero-outside-range convention handles both endpoints.

4.1givenF1step 2.1algebra∎

In three dimensions the primitive product factors into the product of its three one-dimensional coordinate factors. Multiplying their finite expansions gives the stated rectangular index range and a finite expansion in $Λ_{t u v}$ .

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passOpen item page →

Cartesian Gaussian raising, lowering, and kinetic-energy recurrences

Statement

For $g_{α, a, A}$ from Cartesian Gaussian primitives, contractions, and integral conventions, let $e_{j}$ be the $j$ th coordinate vector. With terms having negative indices interpreted as zero, $\partial_{x_{j}} g_{α, a, A} = α_{j} g_{α - e_{j}, a, A} - 2 a g_{α + e_{j}, a, A}, \partial_{A_{j}} g_{α, a, A} = - α_{j} g_{α - e_{j}, a, A} + 2 a g_{α + e_{j}, a, A} .$ The second spatial derivative and kinetic operator are $\partial_{x_{j}}^{2} g_{α, a, A} = α_{j} (α_{j} - 1) g_{α - 2 e_{j}, a, A} - 2 a (2 α_{j} + 1) g_{α, a, A} + 4 a^{2} g_{α + 2 e_{j}, a, A},$ $- \frac{1}{2} Δ g_{α, a, A} = \sum_{j = 1}^{3} (- \frac{α_{j} (α_{j} - 1)}{2} g_{α - 2 e_{j}, a, A} + a (2 α_{j} + 1) g_{α, a, A} - 2 a^{2} g_{α + 2 e_{j}, a, A}) .$ Consequently every kinetic integral of finite contractions is a finite linear combination of overlap integrals with these shifted multi-indices.

Facts & Assumptions

Given: A primitive $g_{α, a, A}$ with $a > 0$ as in Cartesian Gaussian primitives, contractions, and integral conventions, and the integral definitions there.

[F1]

Cartesian Gaussian primitives, contractions, and integral conventions: $g_{α, a, A} (x) = (x - A)^{α} e^{- a ∥ x - A ∥^{2}}$ and $T (ϕ, ψ) = - \frac{1}{2} \int \overline{ϕ} Δ ψ$ .

[F2]

Absolute convergence and local parameter domination for Gaussian basis integrals: each shifted primitive and the corresponding kinetic integrand are absolutely integrable.

[L9]

Proof

1.1givenF1algebraL9

Differentiate the product $(x_{j} - A_{j})^{α_{j}} e^{- a (x_{j} - A_{j})^{2}}$ . The polynomial derivative contributes $α_{j} g_{α - e_{j}}$ and the exponential derivative contributes $- 2 a g_{α + e_{j}}$ , proving the spatial formula. Differentiating with respect to $A_{j}$ reverses the polynomial derivative sign and changes the exponential derivative to $+ 2 a (x_{j} - A_{j})$ , proving the center formula.

2.1step 1.1algebraL9

Differentiate the spatial formula once more. The derivative of the lower term is $α_{j} (α_{j} - 1) g_{α - 2 e_{j}} - 2 a α_{j} g_{α}$ and the derivative of the raised term is $- 2 a (α_{j} + 1) g_{α} + 4 a^{2} g_{α + 2 e_{j}}$ . Combining the two middle coefficients gives $- 2 a (2 α_{j} + 1)$ and proves the second-derivative formula.

3.1givenF1F2step 2.1algebraL9∎

Multiplying the second-derivative identity by $- 1 / 2$ and summing over $j$ gives the displayed Laplacian formula pointwise. By [F2], all shifted terms are integrable, so substituting this finite sum into the kinetic integral and using finite linearity expresses it as the asserted finite combination of overlaps. Conjugation and finite contraction sums preserve the identity.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passOpen item page →

Positive Coulomb bilinear form, Cauchy–Schwarz, and screening bound

Statement

For pair densities $f, g$ arising as finite products of Gaussian contractions in Cartesian Gaussian primitives, contractions, and integral conventions, let $C (f, g) = \int_{R^{3}} \int_{R^{3}} \frac{\overline{f (x)} g (y)}{∥ x - y ∥_{2}} d y d x .$ Then $C$ is a well-defined Hermitian positive-semidefinite sesquilinear form on their finite linear span, and $∣ C (f, g) ∣^{2} \leq C (f, f) C (g, g) .$ For orbitals $ϕ_{a}, ϕ_{b}, ϕ_{c}, ϕ_{d}$ and pair densities $f_{a b} = \overline{ϕ_{a}} ϕ_{b}$ , the integral convention in Cartesian Gaussian primitives, contractions, and integral conventions gives $∣ G (ϕ_{a}, ϕ_{b}; ϕ_{c}, ϕ_{d}) ∣ \leq \sqrt{G (ϕ_{a}, ϕ_{b}; ϕ_{a}, ϕ_{b}) G (ϕ_{c}, ϕ_{d}; ϕ_{c}, ϕ_{d})},$ where each diagonal quantity is nonnegative. For the real finite energy functional in Finite tensor contractions and their variational energy and gradient, let $C \in R^{n \times r}$ , $D \in R^{r \times r}$ , and define the input-basis density coefficients $W_{a b} = \sum_{p, q = 1}^{r} C_{a p} D_{p q} C_{b q}$ . Here the input basis functions $ϕ_{1}, \dots, ϕ_{n}$ are Gaussian contractions, and the tensor supplied to that functional is required to satisfy $G_{a b c d} = G_{a b, c d} = G (ϕ_{a}, ϕ_{b}; ϕ_{c}, ϕ_{d}) \in R$ . Real-valued contractions in particular give real entries; a primitive basis is the singleton-contraction special case. Reindexing the finite two-body energy gives $E_{2} = \frac{1}{2} \sum_{a, b, c, d} W_{a b} W_{c d} G_{a b, c d}$ . Thus for any finite set $S$ of input-basis quartets omitted from that contraction, $B_{S} = \frac{1}{2} \sum_{(a, b, c, d) \in S} ∣ W_{a b} W_{c d} ∣ \sqrt{G_{a b, a b} G_{c d, c d}}$ is an accumulated upper bound for the absolute omitted energy contribution. This does not assert that a screened integral is zero.

Facts & Assumptions

Given: Gaussian contractions and pair densities from Cartesian Gaussian primitives, contractions, and integral conventions, with all Coulomb integrals interpreted as in that definition.

[F1]

Cartesian Gaussian primitives, contractions, and integral conventions: $G (ϕ, ψ; ρ, σ) = C (\overline{ϕ} ψ, \overline{ρ} σ)$ , where $C (f, g) = \iint \overline{f (x)} g (y) / ∥ x - y ∥ d y d x$ .

[F2]

Absolute convergence and local parameter domination for Gaussian basis integrals: all pair densities are in $L^{1} \cap L^{\infty}$ , and $\iint ∣ f (x) g (y) ∣ / ∥ x - y ∥ d y d x < \infty$ .

[F3]

The Gaussian integral $\int_{- \infty}^{\infty} e^{- x^{2}} d x = \sqrt{π}$ : $\int_{R} e^{- x^{2}} d x = \sqrt{π}$ .

[F4]

Change of variable in an improper integral: a positive scaling substitution preserves a convergent improper integral.

[F5]

Tonelli's theorem for nonnegative measurable functions on a sigma-finite product and Fubini's theorem for L^1 functions on a sigma-finite product: nonnegative and absolutely integrable product integrals may be interchanged with their section integrals.

[F6]

Cauchy-Schwarz inequality for $L^{2}$ : finite Euclidean inner products satisfy Cauchy–Schwarz.

[F7]

Finite tensor contractions and their variational energy and gradient: the real two-body energy is the finite contraction $\frac{1}{2} \sum_{p q r s} D_{p q} D_{r s} G_{p q r s}^{'}$ with four factors of $C$ in $G^{'}$ .

Proof

1.1givenF2F3F4F5algebra

For $r > 0$ , substitute $u = s r$ in the Gaussian integral [F3] and use symmetry to get $\frac{1}{r} = \frac{2}{\sqrt{π}} \int_{0}^{\infty} e^{- s^{2} r^{2}} d s .$ The diagonal $x = y$ is measurable and product-measure null: every section is a singleton, so Tonelli [F5] gives measure zero. By [F2], the absolute Coulomb integrand is integrable; Tonelli [F5] on its nonnegative product with the $s$ -integral therefore permits insertion of the Laplace representation into $C (f, f)$ .

1.2givenF2F5F6algebra

At $s = 0$ the double integral equals $∣ \int f ∣^{2} \geq 0$ ; for $s > 0$ , factor $e^{- s^{2} ∥ x - y ∥^{2}} = e^{- s^{2} ∥ x ∥^{2}} e^{- s^{2} ∥ y ∥^{2}} \prod_{j = 1}^{3} e^{2 s^{2} x_{j} y_{j}} .$ Expanding the three exponentials gives terms $(2 s^{2})^{∣ α ∣} x^{α} y^{α} / α!$ . The pointwise absolute sum after multiplying the Gaussian factors is at most one, because $\sum_{j} ∣ x_{j} y_{j} ∣ \leq ∥ x ∥ ∥ y ∥$ by [F6] and $∥ x ∥^{2} + ∥ y ∥^{2} - 2 ∥ x ∥ ∥ y ∥ = (∥ x ∥ - ∥ y ∥)^{2} \geq 0$ . Its product with $∣ f (x) ∣ ∣ f (y) ∣$ is integrable, with double integral at most $∥ f ∥_{1}^{2}$ . Tonelli and Fubini [F5] therefore permit termwise integration and factor each term, yielding $\int \int \overline{f (x)} f (y) e^{- s^{2} ∥ x - y ∥^{2}} d y d x = \sum_{α \in N_{0}^{3}} \frac{(2 s^{2})^{∣ α ∣}}{α!} {∣ \int f (x) x^{α} e^{- s^{2} ∥ x ∥^{2}} d x ∣}^{2} \geq 0.$

2.1step 1.1step 1.2F2algebra

Integrating the nonnegative quantity in step 1.2 over $s$ with the factor $2 / \sqrt{π}$ from step 1.1 gives $C (f, f) \geq 0$ . Absolute convergence [F2] also makes $C$ Hermitian and sesquilinear.

3.1step 2.1algebra

For $C (g, g) > 0$ , expand $0 \leq C (f + z g, f + z g)$ for arbitrary $z \in C$ and choose $z = - C (g, f) / C (g, g)$ ; the resulting quadratic inequality is $∣ C (f, g) ∣^{2} \leq C (f, f) C (g, g)$ . If $C (g, g) = 0$ and $a = C (f, g) \neq 0$ , choosing $z = - t \overline{a}$ for arbitrarily large real $t > 0$ would give $0 \leq C (f, f) - 2 t ∣ a ∣^{2}$ , a contradiction. Hence $C (f, g) = 0$ and the inequality still holds.

4.1givenF1F7step 3.1algebra∎

By [F1], each two-electron entry is $C (f_{a b}, f_{c d})$ . Applying step 3.1 gives its diagonal Cauchy–Schwarz bound and nonnegative diagonals. Substitute the four $C$ factors from [F7] into the finite two-body energy and reorder its finite sums; the coefficient of $G_{a b, c d}$ is $W_{a b} W_{c d}$ . The absolute omitted contribution is at most the sum of the absolute values of its weighted terms, giving $B_{S}$ . The sum is retained in the report, so no omitted entry is called exactly zero.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passOpen item page →

Hermite recurrence formulas for Gaussian nuclear-attraction and two-electron Coulomb integrals

Statement

For $p > 0$ , $P, C \in R^{3}$ , and $η = p q / (p + q)$ with $p, q > 0$ , the Hermite Coulomb auxiliaries of Hermite Gaussian and Boys Coulomb auxiliary functions satisfy $R_{000}^{n} (p, P - C) = (- 2 p)^{n} F_{n} (p ∥ P - C ∥^{2}),$ $R_{t + 1, u, v}^{n} = (P_{1} - C_{1}) R_{t u v}^{n + 1} + t R_{t - 1, u, v}^{n + 1},$ with the corresponding coordinate formulas for increasing $u$ or $v$ and with negative-index terms zero. The one-center and two-center base Coulomb integrals are $\int_{R^{3}} \frac{e^{- p ∥ x - P ∥^{2}}}{∥ x - C ∥} d x = \frac{2 π}{p} F_{0} (p ∥ P - C ∥^{2}),$ $\int ⁣ ⁣ \int \frac{e^{- p ∥ x - P ∥^{2}} e^{- q ∥ y - Q ∥^{2}}}{∥ x - y ∥} d y d x = \frac{2 π^{5 / 2}}{p q \sqrt{p + q}} F_{0} (η ∥ P - Q ∥^{2}) .$ For a primitive pair expansion $g_{a} g_{b} = \sum_{t u v} E_{a b}^{t u v} Λ_{t u v}$ , the nuclear attraction integral is $V_{C} (g_{a}, g_{b}) = \frac{2 π}{p} \sum_{t u v} E_{a b}^{t u v} R_{t u v}^{0} (p, P - C) .$ For two primitive pairs, with coefficients $E_{a b}$ and $E_{c d}$ and centers $P, Q$ , the Coulomb integral is $G (g_{a}, g_{b}; g_{c}, g_{d}) = \frac{2 π^{5 / 2}}{p q \sqrt{p + q}} \sum_{t u v} \sum_{τ ν ϕ} \overline{E_{a b}^{t u v}} E_{c d}^{τ ν ϕ} (- 1)^{τ + ν + ϕ} R_{t + τ, u + ν, v + ϕ}^{0} (η, P - Q) .$ All sums are finite; the largest Boys order is bounded by the total polynomial degree in the participating primitives.

Facts & Assumptions

Given: Primitive Gaussians and Lebesgue integral conventions from Cartesian Gaussian primitives, contractions, and integral conventions, Hermite and $R^{n}$ definitions from Hermite Gaussian and Boys Coulomb auxiliary functions, and finite pair expansions from Finite Hermite expansion and coefficient recurrences for a Cartesian Gaussian pair.

[F1]

Gaussian product theorem and finite polynomial shifts: $e^{- a ∥ x - A ∥^{2}} e^{- b ∥ x - B ∥^{2}} = e^{- a b ∥ A - B ∥^{2} / (a + b)} e^{- (a + b) ∥ x - P ∥^{2}}$ with $P = (a A + b B) / (a + b)$ .

[F2]

Finite Hermite expansion and coefficient recurrences for a Cartesian Gaussian pair: each Cartesian primitive pair has a finite Hermite-Gaussian expansion with the stated coefficients.

[F3]

Hermite Gaussian and Boys Coulomb auxiliary functions: $Λ_{t u v} = \partial_{P}^{t u v} e^{- p ∥ x - P ∥^{2}}$ and $R_{t u v}^{n} = (- 2 p)^{n} \partial_{P}^{t u v} F_{n} (p ∥ P - C ∥^{2})$ .

[F4]

Boys integral, power series, recurrence, and incomplete-gamma representation: $F_{n}^{'} (T) = - F_{n + 1} (T)$ and $F_{n} (T) = \int_{0}^{1} t^{2 n} e^{- T t^{2}} d t$ .

[F5]

The Gaussian integral $\int_{- \infty}^{\infty} e^{- x^{2}} d x = \sqrt{π}$ and Cartesian Gaussian moments and exponent-parameter derivatives: $\int_{R} e^{- x^{2}} d x = \sqrt{π}$ and $\int_{R^{3}} e^{- p ∥ x ∥^{2}} d x = (π / p)^{3 / 2}$ .

[F6]

Absolute convergence and local parameter domination for Gaussian basis integrals: the Coulomb integrals and all finite center derivatives are absolutely integrable with a common local parameter majorant.

[F7]

Change of variable in an improper integral: a monotone differentiable surjection preserves convergent improper integrals when its derivative and the target integrand are locally Riemann integrable and the proper substitution hypotheses hold on every compact truncation, with singular ends treated separately.

[L8]

Tonelli's theorem for nonnegative measurable functions on a sigma-finite product and Fubini's theorem for L^1 functions on a sigma-finite product permit interchange of nonnegative and absolutely integrable iterated integrals, respectively.

[L9]

Proof

1.1givenF1F5F7L8algebra

For $r > 0$ , the Gaussian integral and substitution $u = s r$ give $r^{- 1} = (2 / \sqrt{π}) \int_{0}^{\infty} e^{- s^{2} r^{2}} d s$ . Insert this representation into the one-center integral; Tonelli applies to the nonnegative integrand. Completing the square in $x$ using [F1] gives a three-dimensional Gaussian integral $(π / (p + s^{2}))^{3 / 2}$ times $e^{- p s^{2} ∥ P - C ∥^{2} / (p + s^{2})}$ . The substitution $t = s / \sqrt{p + s^{2}}$ maps $[0, \infty)$ monotonically onto $[0, 1)$ and simplifies the remaining factor to $2 π / p \int_{0}^{1} e^{- p ∥ P - C ∥^{2} t^{2}} d t$ , which is the stated base formula. Both substitutions are smooth monotone surjections with continuous derivatives and integrands on their compact truncations; the transformed Boys integrand is bounded at $t = 1$ , so [F7] applies at the improper ends.

1.2givenF3F4L9algebrainduction

From [F4] and the chain rule, $\partial_{P_{1}} F_{n} (p ∥ P - C ∥^{2}) = - 2 p (P_{1} - C_{1}) F_{n + 1} (p ∥ P - C ∥^{2})$ . Applying $\partial_{P_{1}}^{t} \partial_{P_{2}}^{u} \partial_{P_{3}}^{v}$ and the product rule to $(P_{1} - C_{1}) F_{n + 1}$ produces one term $(P_{1} - C_{1}) R_{t u v}^{n + 1}$ and $t$ terms $R_{t - 1, u, v}^{n + 1}$ . Multiplying by the normalization $(- 2 p)^{n}$ yields the displayed recurrence; the same argument applies to the other coordinates.

2.1givenF1F5F6L8step 1.1algebra

For the two-center base, set $z = x - y$ and integrate first in $x$ . Completing the square with [F1] gives $\int_{R^{3}} e^{- p ∥ x - P ∥^{2}} e^{- q ∥ x - z - Q ∥^{2}} d x = (π / (p + q))^{3 / 2} e^{- η ∥ z - (P - Q) ∥^{2}} .$ Absolute convergence [F6] justifies the change of variables and order of integration. Applying step 1.1 with exponent $η$ and center difference $P - Q$ , then simplifying $(π / (p + q))^{3 / 2} (2 π / η)$ , gives $2 π^{5 / 2} / (p q \sqrt{p + q})$ times the stated Boys value.

3.1givenF3F6step 1.1step 2.1algebraL9

By [F6], differentiating either base integral with respect to its Gaussian centers is valid for every finite derivative order. Since $Λ_{t u v}$ is exactly the corresponding center derivative by [F3], the one-center Hermite Coulomb integral is $(2 π / p) \partial_{P}^{t u v} F_{0} = (2 π / p) R_{t u v}^{0}$ . In the two-center case, derivatives in $Q$ act on $P - Q$ with a minus sign for each coordinate derivative; hence the Hermite integral is the base constant times $(- 1)^{τ + ν + ϕ} \partial_{P - Q}^{t + τ, u + ν, v + ϕ} F_{0}$ .

4.1givenF1F2step 3.1algebra∎

Substitute the finite expansions from [F2] into the one- and two-center integrals. Linearity makes the sums finite. The one-center Hermite formula from step 3.1 gives the stated nuclear formula, and the two-center formula from step 3.1 gives the displayed signed double sum. Complex contractions use conjugate-linear coefficients in the first pair exactly as in the Coulomb form specified in Given; the primitive formulas are real.

AlgorithmAlgorithm: AI-adaptedProof: Not applicableOpen item page →

Finite-budget certified evaluation of Boys function tables

Definition

Input a nonnegative integer $M$ , a finite dyadic interval $T = [T_{-}, T_{+}] \subset [0, \infty)$ , absolute tolerance $ε_{a} > 0$ , optional relative tolerance $ε_{r} > 0$ , a finite integer work cap $W$ , a finite integer precision cap $P \geq 2$ , and a dyadic format with precision $2 \leq p \leq P$ , exponent bounds and elementary truncation index $K \geq 1$ . These are the backend parameters of Certified special-function enclosure result. The output is a table of real dyadic intervals $I_{m}$ for $0 \leq m \leq M$ , with status success, inconclusive, domain, or range.

All arithmetic uses Outward-rounded interval, rectangle and ball operations. Every real elementary call means a typed DAG call to Certified range evaluation for elementary real and complex functions at the supplied format and fixed $K$ . Embed an exact rational argument by outward rounding; check the domain of the entire rounded argument before calling. Square roots use the outward square-root operation. No machine elementary value is an endpoint certificate. Maintain a shared work counter: charge each arithmetic operation, conversion, comparison, loop update, summand and primitive child operation before executing it. Interrupt a child when the remaining counter reaches zero. A cap exhaustion, unresolved enclosure test, intermediate overflow, or child non-success on otherwise valid data makes the affected seed or directional candidate unavailable; if no candidate succeeds, return inconclusive. Return range only when a certified bound proves that an exact requested table value lies outside the largest finite magnitude of the supplied format. Invalid original inputs give domain; a domain test obscured only by intermediate rounding gives inconclusive.

Validate the stated input conditions and supported format. Process the distinct endpoints in increasing order; process the distinct seed orders $m \in {0, M}$ in increasing order. At an endpoint $τ = 0$ , form the exact rationals $1 / (2 m + 1)$ for every $0 \leq m \leq M$ . If any exact value exceeds the largest finite magnitude of the format, return range; otherwise round the rationals outward to the output format. Use this table without a recurrence. A rational is retained exactly internally, but a non-dyadic rational is not returned as a singleton dyadic interval.
For each positive endpoint $τ$ , perform refinements $k = 0, 1, \dots, W - 1$ , subject to the shared work counter. At refinement $k$ , try the two seed orders separately using their own $m$ and $s = m + \frac{1}{2}$ :
- If $0 < τ \leq 1$ , evaluate the Taylor polynomial through $N = k$ from Boys integral, power series, recurrence, and incomplete-gamma representation, then enlarge by the outward upper bound for $τ^{N + 1} / ((N + 1)! (2 m + 2 N + 3))$ from A monotone-range Taylor remainder for small Boys arguments. The condition $N + 2 \geq τ$ holds throughout this branch.
- If $1 < τ \leq 2 m + 1$ , use $N = 2^{k}$ panels of A positive midpoint enclosure for Boys functions on bounded arguments, in increasing node order $j = 1, \dots, N$ , and enlarge the positive midpoint sum by $(m + τ) / (2 N)$ . Its dyadic nodes are formed exactly before storage; evaluate their exponentials by the finite real elementary call.
- If $τ > 2 m + 1$ , request the Gamma target from Finite certified evaluation of Gamma and a continued log-Gamma branch on the exact rectangle $[s, s] + i [0, 0]$ , with positive exact rational child absolute tolerance $q / 2^{k + 2}$ , where $q$ is constructed by starting at $q = 1$ and repeatedly replacing $q$ by $q / 2$ until $q \leq ε_{a}$ . Charge every comparison and halving to the shared counter; exhaustion returns inconclusive. Thus $0 < q \leq ε_{a}$ without restricting the parent tolerance to rational values. Supply no relative request, base format precision $p_{0} = p$ , the same exponent bounds and fixed elementary truncation $K$ , child precision cap $P$ , and child work cap $w = ⌊ R / 4 ⌋$ , where $R$ is the remaining parent work at call entry. If $w < 1$ , stop inconclusive. Debit its actual work, including unsuccessful work, to the parent counter. A successful child rectangle has real projection containing the real number $Γ (s)$ : its reality follows from the positive-real Euler integral, also evaluated by the half-integer identity in Boys integral, power series, recurrence, and incomplete-gamma representation. Use this projection as the real Gamma enclosure. Evaluate $e^{- τ}$ by the real elementary call, and use A scaled incomplete-gamma tail bound for large Boys arguments to form the enclosing interval for $F_{m} (τ)$ . Compute $τ^{s} = τ^{m} \sqrt{τ}$ and $τ^{s - 1} = τ^{s} / τ$ by outward operations; the exact denominator $1 - \max (s - 1, 0) / τ$ is positive. Replace a negative lower endpoint by zero, retaining the upper endpoint. A child range, a child domain on this valid positive argument, or a child inconclusive invalidates that seed attempt and permits the next bounded refinement; no child status is propagated as a range claim for the Boys output.
A finite seed interval is available to its direction only when its radius is at most $ε_{a}$ . A failed attempt does not invalidate a successfully enclosed seed for the other direction. Every panel and child loop is subject to the counter, even when its formal index bound is very large.
At each refinement obtain one finite real interval $J$ for $e^{- τ}$ . From an available order-zero seed form the upward candidate for orders $0, \dots, M$ ; from an available order- $M$ seed form the downward candidate for orders $M, \dots, 0$ . Use the exact affine recurrence maps in Upward and downward Boys recurrence error amplification bounds: compute each affine image's endpoints by exact rational endpoint arithmetic, then convert those two endpoints outward once. If either conversion overflows, discard that directional candidate at this refinement. Otherwise record the two conversion errors and propagate the lemma's radius bounds, including half their sum at each step. This prescription avoids omitting rounding at intermediate nodes. A table is admissible only if every entry satisfies the propagated bound and the requested absolute and, if requested, zero-excluding relative-radius test. Keep the admissible candidate with smaller maximum radius, ties upward. If neither direction is admissible, continue to the next refinement. Once an endpoint table is chosen, proceed to the next endpoint. No upward division is attempted at zero.
With both endpoint tables, form $I_{m} = hull (I_{m} (T_{+}), I_{m} (T_{-}))$ for every requested order, using endpoint minima and maxima. By $F_{m}^{'} (T) = - F_{m + 1} (T) < 0$ from Boys integral, power series, recurrence, and incomplete-gamma representation, this encloses the full range over $T$ . Return success only after every output radius is at most $ε_{a}$ and, when relative tolerance is requested, the interval excludes zero and satisfies the relative-radius test in Certified special-function enclosure result. Otherwise return inconclusive. Exhausting the finite refinement list or shared work counter also returns inconclusive. At a positive endpoint, return range only if a certified lower bound for some requested exact Boys value exceeds the largest finite magnitude of the format; a merely overflowing enclosure endpoint gives inconclusive. No branch promises success for every valid box or finite cap.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passOpen item page →

Soundness of every successful finite-budget Boys enclosure

Statement

Every call to Finite-budget certified evaluation of Boys function tables terminates after finitely many operations bounded by its declared caps. Whenever it returns success on $T \subset [0, \infty)$ , each returned interval $I_{m}$ contains the exact range ${F_{m} (T) : T \in T}$ for $0 \leq m \leq M$ and has the absolute and any reported relative accuracy required by Certified special-function enclosure result. It may instead return inconclusive, domain, or range; no success for every finite input or cap is asserted.

Facts & Assumptions

Given: An invocation of Finite-budget certified evaluation of Boys function tables with finite outward interval operations. For the enclosure assertions assume its return is success; the termination argument also covers unsuccessful returns.

[F1]

Finite-budget certified evaluation of Boys function tables: the branch order is Taylor for $T \leq 1$ , positive midpoint for $1 < T \leq 2 m + 1$ , and scaled incomplete-gamma tail for $T > 2 m + 1$ ; table values are then propagated upward or downward and interval inputs are handled by endpoint hulls.

[F2]

Certified special-function enclosure result: a success interval contains the exact requested range, has radius at most the absolute tolerance, and claims relative accuracy only when zero is excluded and the relative-radius test passes.

[F3]

A monotone-range Taylor remainder for small Boys arguments: in the stated monotone-term range, the Taylor partial sum plus its first omitted term encloses $F_{m} (T)$ .

[F4]

A positive midpoint enclosure for Boys functions on bounded arguments: the positive midpoint sum plus/minus $(m + T) / (2 N)$ encloses $F_{m} (T)$ .

[F5]

A scaled incomplete-gamma tail bound for large Boys arguments: the scaled incomplete-gamma interval contains $F_{m} (T)$ on the large branch.

[F6]

Finite certified evaluation of Gamma and a continued log-Gamma branch and Soundness of finite Gamma and log-Gamma enclosures: a successful Gamma request at a positive half-integer returns a rectangle containing that Gamma value. The finite algorithm has bounded child calls; its capped termination and soundness are supplied by the theorem.

[F7]

Certified range evaluation for elementary real and complex functions, Outward-rounded operations are inclusion-isotone and enclose DAG evaluations, and Certified real elementary-function evaluations enclose their ranges: the explicitly called finite typed evaluator and outward arithmetic are sound; in particular, every finite real exponential range interval contains the exact exponential value or range supplied to it.

[F8]

Boys integral, power series, recurrence, and incomplete-gamma representation: $F_{m}^{'} (T) = - F_{m + 1} (T) < 0$ , and the upward and downward recurrences are exact for $T > 0$ .

[F9]

Upward and downward Boys recurrence error amplification bounds: every finite recurrence interval contains the target value and its radius is bounded by the propagated seed and endpoint-rounding errors.

[F10]

Certified special-function enclosure result: work and precision caps are finite, and exhausting a cap returns inconclusive rather than making an uncertified claim.

Proof

1.1givenF1F3F4F7

If an endpoint is zero, the internal rational is exactly $F_{m} (0)$ and its outward-rounded interval contains that value. Each positive-endpoint seed branch uses its own explicitly bound order $m \in {0, M}$ . If the small- $T$ branch is used, [F3] encloses its Taylor sum by its first omitted term. If the positive midpoint branch is used, each exponential node is enclosed by [F7] and the quadrature remainder in [F4] encloses the integral. Thus every successful direct seed interval contains its Boys value.

1.2givenF1F5F6F7F8

In the large branch, [F6] encloses $Γ (m + \frac{1}{2})$ whenever its Gamma call succeeds. This target is real by the positive-real Euler integral and half-integer identity in [F8], so projection onto the real coordinate preserves its enclosure. The prescribed square roots and powers enclose the positive scaling factors by [F7], which also encloses $e^{- T}$ , and [F5] bounds the omitted upper incomplete-gamma tail. Outward interval operations therefore produce a containing interval for $F_{m} (T)$ .

2.1F1F8F9step 1.1step 1.2induction

For $T > 0$ , apply the exact recurrence identities [F8] to each previously enclosed order. The outward interval expression encloses the exact affine recurrence image, and [F9] bounds the stored radius, since the procedure forms each affine endpoint exactly rationally and adds both final outward-conversion errors. Induction over the finite order count proves every entry of either accepted candidate table contains its exact Boys value.

3.1givenF1F2F8step 2.1algebra

For $T_{-} \leq T \leq T_{+}$ , [F8] makes $F_{m}$ decreasing, so its exact range lies between its endpoint values. The endpoint hull in [F1] therefore contains the entire range. The algorithm returns success only after the interval tests in [F2]; its other statuses make no success claim.

4.1givenF1F6F7F10algebra∎

The algorithm visits only two endpoints and $M + 1$ requested orders. Its refinement index is bounded by $W$ ; Taylor sums, midpoint panels and recurrence tables each have finite indices. More strongly, the shared counter is checked before every primitive operation and loop update, including all work inside Gamma and elementary subcalls. Every child receives the specified finite format/truncation inputs and the Gamma child additionally receives a finite work cap no larger than the remaining parent budget. Thus even a child whose complete construction would exceed that budget is interrupted with inconclusive; every branch returns a status after finitely many charged operations. No argument infers success from the size of a finite cap.

AlgorithmAlgorithm: AI-adaptedProof: Not applicableOpen item page →

Finite primitive and contracted Gaussian integral evaluation with certified screening

Definition

Inputs. A finite list of input basis contractions $ϕ_{a} = \sum_{i = 1}^{q_{a}} d_{a i} g_{a i}$ , $1 \leq a \leq n$ , from Cartesian Gaussian primitives, contractions, and integral conventions, represented by finite dyadic intervals for real centers and positive exponents and finite dyadic intervals or complex rectangles for coefficients; a finite nuclear list $((C_{ℓ}, w_{ℓ}))_{ℓ = 1}^{J}$ whose centers and signed real weights are represented by finite dyadic intervals; a requested subset $I \subseteq {S, T, V, G}$ of integral outputs (overlap, kinetic, nuclear attraction, and Coulomb); and Boolean energy and gradient requests, with a gradient request requiring an energy request. Require at least one requested output. Supply a positive integral tolerance $ε_{I}$ for every requested integral and for integrals used internally by an energy request; supply a positive energy tolerance $ε_{E}$ when energy is requested and, for a gradient request, an optional positive gradient tolerance defaulting to $ε_{E}$ . An optional positive screening tolerance is allowed only for an energy request. Also supply finite positive integer work and precision caps $W, P$ and a dyadic format of precision $2 \leq p \leq P$ with exponent bounds and fixed elementary truncation index $K \geq 1$ . A primitive request is the singleton-contraction case. An energy/gradient request additionally requires $n, r \geq 1$ , real primitive-contraction coefficients $d_{a i}$ and real nuclear data, real matrices $C \in R^{n \times r}, D \in R^{r \times r}$ given by dyadic boxes (exact matrices are singleton boxes), and uniform finite bounds $B \geq \sup ∥ C ∥_{F}$ , $M_{D} \geq \sup ∥ D ∥_{F}$ from Finite tensor contractions and their variational energy and gradient. Internal primitive labels $(a, i)$ are distinct from the input basis labels $a$ ; $C$ is a subsequent transform of the input basis.

Outputs. A status success, inconclusive, domain, or range; outward real intervals or complex rectangles for the integrals in $I$ ; an energy interval when energy is requested; a gradient center and Frobenius gradient-error bound when gradient is requested; and a separately accumulated discarded-energy bound when screening is enabled. Success encloses every parameter value in the input boxes. No status declares an omitted integral zero.

Finite calls and accounting. Use Outward-rounded interval, rectangle and ball operations for arithmetic. Every real elementary call means a typed DAG call to Certified range evaluation for elementary real and complex functions at the supplied format and $K$ . Enclose $π$ by the Machin identity in Trigonometric identities, Machin's formula and reduced Taylor tails and the $K$ -term arctangent series with geometric tails from Range-reduced exponential, logarithm and arctangent series have certified tails, using exact rational tail endpoints before final outward conversion. A shared counter charges each conversion, comparison, loop update, arithmetic operation, recurrence update and summand, including every primitive operation executed by a child. Check the counter before executing an operation and interrupt any child at exhaustion. A required Boys call receives remaining work $R$ as its finite work cap, precision cap $P$ , the same format and $K$ , absolute tolerance $ε_{I} / 2$ and no relative request; its actual work is charged to the parent. A required child non-success on otherwise valid data or an intermediate overflow makes the current integral evaluation inconclusive; a rounded intermediate failing a domain certification on valid original data is also inconclusive. Return range only when a certified lower bound for a requested exact output component exceeds the largest finite magnitude of the format or a certified upper bound is below its negative. A mere overflow of a conservative intermediate or enclosure endpoint is not enough to claim range. Invalid original inputs return domain; cap exhaustion returns inconclusive. These choices are conservative and need not permit success under every cap or tolerance.

Validate the request specification, positive exponent lower endpoints, finite input boxes, indices in $N_{0}^{3}$ , supported format and positive tolerances/caps. Invalid original data return domain. If energy/gradient is requested, verify realness and dimensions and certify the norm bounds by outward Frobenius upper bounds on the complete boxes. If this sufficient norm test cannot certify the supplied bounds, return inconclusive; do not claim that an unknown represented matrix violates its bound. Form finite primitive-pair and quartet lists for the requested integrals and any energy/gradient dependencies, lexicographically. Include all shifted overlap pairs required by the kinetic raising/lowering formula; a negative index contributes zero.
For each ordered primitive pair with exponents $a, b$ , indices $α, β$ and centers $A, B$ , compute $p = a + b$ , $P = (a A + b B) / p$ , and $K_{a b} = \exp (- a b ∥ A - B ∥^{2} / p)$ by outward arithmetic and the real elementary call. Compute the Hermite coefficients by Finite Hermite expansion and coefficient recurrences for a Cartesian Gaussian pair, raising the first primitive in x,y,z order and then the second, storing each intermediate degree table until its successors have been formed. The final table has $\prod_{j = 1}^{3} (α_{j} + β_{j} + 1)$ entries; every intermediate table update is also charged. Compute overlap by the finite shifted polynomial expansion and the moments in Cartesian Gaussian moments and exponent-parameter derivatives, and kinetic by Cartesian Gaussian raising, lowering, and kinetic-energy recurrences. Certified square roots and integer powers evaluate all half-integer factors in those moment formulas.
To evaluate an attraction primitive pair, put $L = ∣ α ∣ + ∣ β ∣$ and use exponent $η = p$ and center difference $P - C_{n u c}$ . To evaluate a primitive Coulomb quartet, including any diagonal self quartet, put $L = ∣ α ∣ + ∣ β ∣ + ∣ γ ∣ + ∣ δ ∣$ , $η = p q / (p + q)$ and center difference $P - Q$ , where the second pair has exponent $q$ . Form the nonnegative Boys argument interval $T = η ∥ P - Q ∥^{2}$ , with the evident attraction substitution, using interval squaring and the positive exponent bounds. Request Boys orders $0, \dots, L$ from Finite-budget certified evaluation of Boys function tables. If rounding prevents certification of a required positive denominator, return inconclusive.
Initialize $R_{000}^{j} = (- 2 η)^{j} F_{j} (T)$ for $0 \leq j \leq L$ . For total derivative degree $d = 1, \dots, L$ , enumerate $(t, u, v)$ lexicographically with $t + u + v = d$ , choose its first nonzero coordinate in x,y,z order, and apply that coordinate's recurrence in Hermite recurrence formulas for Gaussian nuclear-attraction and two-electron Coulomb integrals for $0 \leq j \leq L - d$ . Negative-index terms are zero. For example, when $t > 0$ , use $R_{t u v}^{j} = (P_{1} - Q_{1}) R_{t - 1, u, v}^{j + 1} + (t - 1) R_{t - 2, u, v}^{j + 1}$ . Each predecessor is at a smaller derivative degree and within its stored Boys-order range. Contract the finite Hermite sums in that theorem to get each primitive integral.
Contract primitive integrals to input-basis integrals by the finite coefficient sums. For overlap, kinetic and attraction the coefficient is $\overline{d_{a i}} d_{b j}$ . For the defined pair-density Coulomb convention, the primitive quartet coefficient is $d_{a i} \overline{d_{b j}} \overline{d_{c k}} d_{d l}$ : expand $\overline{f_{a b} (x)} f_{c d} (y)$ in Cartesian Gaussian primitives, contractions, and integral conventions. In the real energy branch these are the four real contraction coefficients. Cache only identical ordered parameter boxes, angular indices, format and truncation context; an $R$ cache record also stores its cutoff $L$ . Reuse a table only if its stored cutoff is at least the needed cutoff; otherwise compute the larger table under the counter.
Optional Coulomb-energy screening applies to whole input-basis quartets, before their off-diagonal primitive quartets are evaluated. First compute every required contracted diagonal $G_{a b, a b}$ without screening by steps 2–5, including all coefficients $d$ . Obtain finite nonnegative upper endpoints $U_{a b}$ from their real projections, justified by Positive Coulomb bilinear form, Cauchy–Schwarz, and screening bound. Form the outward real interval $W_{a b} = \sum_{p, q} C_{a p} D_{p q} C_{b q}$ and its upper absolute bound $A_{a b} = \max (∣ \inf W_{a b} ∣, ∣ \sup W_{a b} ∣)$ . Compute nonnegative outward upper bounds $Q_{a b c d} \geq \sqrt{U_{a b} U_{c d}}$ and $w_{a b c d} \geq \frac{1}{2} A_{a b} A_{c d} Q_{a b c d}$ . Enumerate all ordered candidate basis quartets lexicographically, with no unrecorded symmetry compression. Skip a quartet only if the outward accumulated sum after adding $w_{a b c d}$ is at most the screening tolerance; otherwise compute its primitive sums. Store a skipped real entry as $[- Q_{a b c d}, Q_{a b c d}]$ and report the actual accumulated weighted sum. Thus entrywise radius uses $Q$ , while the discarded-energy bound uses $w$ . Even a skipped integral must pass its requested integral-tolerance test. No screening is required or performed when this optional real-energy branch is absent.
If energy or gradient is requested, form the one-body matrix on the input basis by $H_{a b} = T_{a b} + \sum_{ℓ = 1}^{J} w_{ℓ} V_{C_{ℓ}} (ϕ_{a}, ϕ_{b})$ , using the supplied signed nuclear weights, and form the Coulomb tensor $G$ on that basis. Use the midpoint tensors $\tilde{H}, \tilde{G}$ and largest entrywise radii $ε_{2}, ε_{4}$ , including every screened interval. Evaluate the finite polynomial $E (C; D, \tilde{H}, \tilde{G})$ by outward arithmetic over the full $C, D$ boxes, and enlarge its interval by $δ_{E} = M_{D} r n B^{2} ε_{2} + \frac{1}{2} M_{D}^{2} r^{2} n^{2} B^{4} ε_{4}$ from Explicit finite-dimensional contraction error bounds for energy and gradient. If gradient is requested, evaluate every formal partial derivative of this same finite polynomial by differentiating its two and four factors of $C$ and using outward finite sums. If their intervals have midpoints $c_{a μ}$ and radii $ρ_{a μ}$ , return gradient center $c$ with outward upper Frobenius error bound $\sqrt{\sum_{a, μ} ρ_{a μ}^{2}} + δ_{\nabla}$ , where $δ_{\nabla} = 2 n r B M_{D} ε_{2} + 2 n^{2} r^{2} B^{3} M_{D}^{2} ε_{4}$ . This includes uncertainty in $C, D$ as well as integral error; nuclear and contraction-coefficient uncertainty was already included in the integral boxes. Count all these operations. If a final certified bound proves that a requested output range lies wholly outside the finite format, return range; a final endpoint overflow without this proof returns inconclusive. Return success only when every requested integral radius, energy radius and gradient-error bound meets its own declared tolerance; all remaining failures return inconclusive.

An $R$ table with cutoff $L$ stores $\sum_{d = 0}^{L} (L - d + 1) (\binom{d + 2}{2})$ entries. All input, pair, primitive-quartet and auxiliary tables are finite. Every update and child evaluation is also subject to the shared finite work counter, so valid inputs may return inconclusive when their tolerance or work requirement cannot be certified.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passOpen item page →

Soundness and accumulated error bounds for the finite Gaussian integral evaluator

Statement

Every invocation of Finite primitive and contracted Gaussian integral evaluation with certified screening terminates after finitely many operations bounded by its work and child-evaluator caps. If it returns success, each integral interval contains the exact integral range over the supplied parameter boxes. For the real energy/gradient branch, the returned energy interval and gradient-error bound contain the corresponding values of the finite functional in Finite tensor contractions and their variational energy and gradient. The reported discarded-energy bound is at least the sum of the absolute Cauchy–Schwarz bounds for all skipped terms. The evaluator may return inconclusive, domain, or range; no universal success or exact-sparsity claim is made.

Facts & Assumptions

Given: An invocation of Finite primitive and contracted Gaussian integral evaluation with certified screening. For the enclosure assertions assume a successful return on finite dyadic parameter boxes with strictly positive exponent lower bounds; the termination argument also covers unsuccessful returns.

[F1]

Finite primitive and contracted Gaussian integral evaluation with certified screening specifies primitive angular cutoffs, coefficient-weighted contraction to the input basis, a shared work counter including children, and basis-quartet screening by uniform diagonal and density-coefficient upper bounds.

[F2]

Hermite recurrence formulas for Gaussian nuclear-attraction and two-electron Coulomb integrals: the finite Hermite formulas equal the exact Gaussian attraction and Coulomb integrals.

[F3]

Cartesian Gaussian raising, lowering, and kinetic-energy recurrences and Cartesian Gaussian moments and exponent-parameter derivatives: the finite shifted-overlap and kinetic formulas equal their exact integrals.

[F4]

Soundness of every successful finite-budget Boys enclosure: every successful Boys request encloses the exact Boys range on its input interval.

[F5]

Certified special-function enclosure result and Outward-rounded operations are inclusion-isotone and enclose DAG evaluations: each finite outward interval expression contains every exact value from its input boxes; non-finite statuses make no finite claim.

[F8]

Certified real elementary-function evaluations enclose their ranges and Trigonometric identities, Machin's formula and reduced Taylor tails: finite real exponential intervals and a certified interval for $π$ are available for the procedure's constants.

[F6]

Positive Coulomb bilinear form, Cauchy–Schwarz, and screening bound: each omitted Coulomb entry has absolute value at most its diagonal Cauchy–Schwarz product, and the omitted energy is bounded by the sum of its weighted entry bounds.

[F7]

Explicit finite-dimensional contraction error bounds for energy and gradient: entrywise one- and four-index errors give the stated explicit energy and gradient bounds.

Proof

1.1givenF1F2F3F4induction

For overlap and kinetic entries, the procedure's binomial polynomial expansion and shifted moments are exact by [F3]; the pointwise derivative recurrence gives the kinetic identity. For attraction and two-electron entries, [F2] identifies the finite Hermite sums with the exact integrals. Every Boys input interval used in those sums is enclosed by [F4]. For attraction the cutoff is the sum of the two primitive angular degrees; for Coulomb it is the sum of all four. These dominate every Hermite derivative degree in [F2]. At derivative degree $d$ , an entry with $j \leq L - d$ uses predecessors of smaller derivative degree and index $j + 1 \leq L - (d - 1)$ , so induction proves every required $R$ entry is available and enclosed. Finite contraction then uses $\overline{d_{a i}} d_{b j}$ for the one-body integrals and $d_{a i} \overline{d_{b j}} \overline{d_{c k}} d_{d l}$ for this definition's sesquilinear pair-density Coulomb convention; these are precisely the coefficients obtained by expanding the defining integrands.

1.2F1F6algebra

The unscreened contracted diagonal intervals contain $G_{a b, a b}$ including all primitive contraction coefficients. Positivity in [F6] therefore gives $0 \leq G_{a b, a b} \leq U_{a b}$ uniformly on the parameter boxes. Each skipped entry is assigned the interval $[- Q_{a b c d}, Q_{a b c d}]$ with $Q_{a b c d} \geq \sqrt{U_{a b} U_{c d}}$ , which contains it by [F6]. The density interval gives $∣ W_{a b} ∣ \leq A_{a b}$ uniformly, so its weighted absolute energy contribution is at most $w_{a b c d} \geq \frac{1}{2} A_{a b} A_{c d} Q_{a b c d}$ . Adding these bounds over the actual ordered skipped quartets, as done before each screen decision, bounds their entire omitted contribution. The reported outward sum dominates that sum; entrywise $Q$ is not confused with weighted $w$ . No statement sets an omitted integral equal to zero.

2.1F1F5F8step 1.1induction

The recurrence arrays and contractions are finite expression graphs. The exponential and $π$ constants used in those graphs are enclosed by [F8], and every remaining finite interval node encloses the exact node value by [F5]. Combining this induction with step 1.1 proves that every returned integral interval contains its exact range over the input boxes.

3.1F1F5F7step 2.1step 1.2

The midpoint tensors and radii from step 2.1 satisfy the entrywise error hypotheses of [F7], including the screened entries. For every fixed parameter choice, [F7] bounds the integral-tensor contribution to energy and gradient error uniformly using $B, M_{D}$ . The finite polynomial evaluations over the complete $C, D$ boxes contain the midpoint-tensor energy and every component of its gradient. Enlarging the former by $δ_{E}$ contains the exact energy. The gradient component intervals lie within Frobenius distance $\sqrt{\sum ρ_{a μ}^{2}}$ of their returned midpoint center; the triangle inequality adds $δ_{\nabla}$ and gives the reported gradient bound, including input-matrix uncertainty. All final enlargements and norm upper bounds are rounded outward by [F5].

4.1givenF1F4F5algebra∎

All primitive, pair, quartet, Boys-order, and auxiliary-table loops range over finite input lists or the finite integer bounds stated in [F1]. The shared work counter is checked before every primitive operation and loop update, including operations inside Boys, Gamma and elementary subcalls. A child receives finite algorithm parameters and no more than the remaining parent work, and is interrupted when that counter is exhausted by [F1]. Thus a large child construction cannot escape the finite parent cap. Therefore every invocation returns a finite status after finitely many operations.

5 · Examples, counterexamples and false statements

None yet.

Gaussian basis integral recurrences and boys error

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

Cartesian Gaussian primitives, contractions, and integral conventions

Definition

Remarks

Boys functions and lower incomplete-gamma notation

Definition

Finite tensor contractions and their variational energy and gradient

Definition

Gaussian product theorem and finite polynomial shifts

Statement

Facts & Assumptions

Proof

Boys integral, power series, recurrence, and incomplete-gamma representation

Statement

Facts & Assumptions

Proof

A positive midpoint enclosure for Boys functions on bounded arguments

Statement

Facts & Assumptions

Proof

Cartesian Gaussian moments and exponent-parameter derivatives

Statement

Facts & Assumptions

Proof

Explicit finite-dimensional contraction error bounds for energy and gradient

Statement

Facts & Assumptions

Proof

Hermite Gaussian and Boys Coulomb auxiliary functions

Definition

Absolute convergence and local parameter domination for Gaussian basis integrals

Statement

Facts & Assumptions

Proof

A monotone-range Taylor remainder for small Boys arguments

Statement

Facts & Assumptions

Proof

A scaled incomplete-gamma tail bound for large Boys arguments

Statement

Facts & Assumptions

Proof

Upward and downward Boys recurrence error amplification bounds

Statement

Facts & Assumptions

Proof

Finite Hermite expansion and coefficient recurrences for a Cartesian Gaussian pair

Statement

Facts & Assumptions

Proof

Cartesian Gaussian raising, lowering, and kinetic-energy recurrences

Statement

Facts & Assumptions

Proof

Positive Coulomb bilinear form, Cauchy–Schwarz, and screening bound

Statement

Facts & Assumptions

Proof

Hermite recurrence formulas for Gaussian nuclear-attraction and two-electron Coulomb integrals

Statement

Facts & Assumptions

Proof

Finite-budget certified evaluation of Boys function tables

Definition

Soundness of every successful finite-budget Boys enclosure

Statement

Facts & Assumptions

Proof

Finite primitive and contracted Gaussian integral evaluation with certified screening

Definition

Soundness and accumulated error bounds for the finite Gaussian integral evaluator

Statement

Facts & Assumptions

Proof

5 · Examples, counterexamples and false statements

Sources