LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedprecheck pass

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.

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.

Depends on

Used by

Dependency tree · two levels

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

Sources

Trygve Helgaker, Molecular Integral Evaluation, 10th Sostrup Summer School lecture notes (2008) (standard reference, not scraped)
L. E. McMurchie and E. R. Davidson, One and Two Electron Integrals over Cartesian Gaussian Functions, UCRL-13791 (1976) (standard reference, not scraped)