Alphabeta MathHow 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.
Soundness of the finite Fresnel, erf, and Gauss-series enclosures
Statement
If Finite certified power-series evaluation for Fresnel, erf, and Gauss functions returns success for
, or a Gauss-series value on its stated domain, its
returned interval or rectangle contains that exact function value and passes
the requested absolute-radius test. A relative certificate is valid only when
the enclosure excludes zero and the contract's relative-radius test passes.
Every execution with finite caps terminates. The theorem makes no claim of success for every valid input.
Facts & Assumptions
Given: A successful return of the procedure in Finite certified power-series evaluation for Fresnel, erf, and Gauss functions with a sound outward interval backend.
Outward-rounded interval, rectangle and ball operations and Outward-rounded operations are inclusion-isotone and enclose DAG evaluations: every finite interval operation encloses its exact rational or interval result.
Certified range evaluation for elementary real and complex functions is the finite subroutine used for sqrt-pi range evaluation; its finite real and complex outputs are sound by Certified real elementary-function evaluations enclose their ranges and Certified complex exponential and principal logarithm enclose their ranges.
Finite certified power-series evaluation for Fresnel, erf, and Gauss functions: a successful series branch encloses its finite partial sum and enlarges it by the applicable geometric tail bound before applying the radius test.
Fresnel, error, and Gauss hypergeometric series: the four functions on the stated branches are represented by the specified series.
Fresnel series geometric tail bounds: the Fresnel tail bound contains the exact omitted series tail when the tested ratio is below .
Error-function series geometric tail bound: the tail bound contains the exact omitted series tail when the tested ratio is below .
Gauss hypergeometric series geometric tail bound: the Gauss tail bound contains the exact omitted series tail when and ; terminating parameter cases have zero tail after their last nonzero term.
Certified special-function enclosure result: the radius and relative
tests specify exactly which claims accompany success.
Proof
In each nonterminating success branch, the exact value is the sum of the partial series and its omitted tail by the series definitions in the algorithm contract. The relevant lemma among [F3], [F4], and [F5] bounds the modulus of that tail by the radius used to enlarge the partial-sum enclosure. In a terminating Gauss branch [F5] makes the tail exactly zero.
The outward interval backend encloses the exact arithmetic partial sums by [A1]. Every elementary-range subcall used for constants or interval images is sound by [A2]. Adding the symmetric tail enlargement therefore gives an interval or rectangle containing the exact full value.
The procedure reports success only after the containing enclosure passes the absolute-radius test; its relative flag is set only under the stated zero-exclusion and relative-radius conditions. These are exactly the certificate claims in [F6]. If no candidate passes, the procedure returns inconclusive; no universal success is asserted.
The outer stage count is finite, each partial sum has at most the capped number of terms, and each elementary-range call has a finite DAG, format, and truncation index. Thus every capped execution terminates.
Depends on
- Finite certified power-series evaluation for Fresnel, erf, and Gauss functions
- Certified range evaluation for elementary real and complex functions
- Certified special-function enclosure result
- Fresnel, error, and Gauss hypergeometric series
- Outward-rounded interval, rectangle and ball operations
- Fresnel series geometric tail bounds
- Error-function series geometric tail bound
- Gauss hypergeometric series geometric tail bound
- Outward-rounded operations are inclusion-isotone and enclose DAG evaluations
- Certified real elementary-function evaluations enclose their ranges
- Certified complex exponential and principal logarithm enclose their ranges
Used by
Cited to discharge well-definedness by Finite certified power-series evaluation for Fresnel, erf, and Gauss functions.
Dependency tree · two levels
36 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
- DLMF, §15.2(i), Gauss series (standard reference, not scraped)
- DLMF, §§7.6(i) and 15.2(i) (standard reference, not scraped)
- N. M. Temme, “Numerical aspects of special functions,” Acta Numerica 17 (2008), §2 (standard reference, not scraped)