TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-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.

Soundness of finite integer-order Bessel enclosures

Statement

Whenever Finite certified evaluation of integer-order Bessel functions returns success, its interval contains the requested $J_{n} (x)$ or scaled modified Bessel value $e^{- x} I_{n} (x)$ and passes the requested absolute-radius test. A relative certificate is valid only when zero is outside the interval and the relative test passes. The theorem makes no success guarantee for every input or finite cap. Every execution with finite caps terminates.

Facts & Assumptions

Given: A successful return of Finite certified evaluation of integer-order Bessel functions with a sound outward interval backend.

[A1]

Certified range evaluation for elementary real and complex functions supplies the finite real sine, cosine, and exponential ranges used by the midpoint branches; every finite range is sound by Certified real elementary-function evaluations enclose their ranges.

[A2]

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

[F1]

Finite certified evaluation of integer-order Bessel functions: series, midpoint, and finite Miller candidates are returned only after their respective tail or terminal-error enclosures are applied; its exact scaled- $I$ input $x = 0$ branch returns the corresponding defining-series value. Candidate intersections are taken only when nonempty.

[F2]

Integer-order Bessel series and Real elementary functions and their domains: at $x = 0$ , the defining series gives $I_{0} (0) = 1$ , $I_{n} (0) = 0$ for $n \geq 1$ , and $e^{0} = 1$ .

[F3]

Certified special-function enclosure result: success requires exact inclusion and the stated radius; relative certification requires zero exclusion.

[F4]

Convergence and geometric tails for integer-order Bessel series: the truncated $J_{n}$ series tail is enclosed by the geometric bound when its ratio test passes.

[F5]

Exact finite terminal-contamination error identity: the finite normalized backward recurrence error is exactly the displayed terminal-contamination expression whenever its denominators are nonzero.

[F6]

Composite midpoint enclosure for the integer Bessel integral: the midpoint $J_{n}$ enclosure contains the exact cosine integral.

[F7]

Composite midpoint enclosure for the scaled modified Bessel integral: the midpoint enclosure contains the exact scaled $I_{n}$ integral.

[F8]

Trigonometric identities, Machin's formula and reduced Taylor tails supplies the Machin identity; the arctangent series and geometric-tail argument in Range-reduced exponential, logarithm and arctangent series have certified tails give the finite bounds used to enclose $π$ for the midpoint mesh.

[F9]

Complementary solution for the integer Bessel recurrence: $D_{0} = - J_{1}$ , $D_{1} = J_{0}$ , and $D_{j + 1} = 2 j D_{j} / x - D_{j - 1}$ for $x > 0$ and $j \geq 1$ .

Proof

1.1A1A2F1F2F4F6F7F8

If the target is scaled $I$ and $x = 0$ , the defining series [F2] gives $e^{- x} I_{n} (x) = 1$ for $n = 0$ and $0$ for $n \geq 1$ , so the exact internal singleton contains the target; its final outward conversion also contains it by [A2], and the algorithm tests the actual rounded radius. Otherwise, the power-series candidate contains $J_{n} (x)$ by [F4]. The two midpoint candidates contain their integrals by [F6] and [F7]; their finite sine, cosine, and exponential ranges are sound by [A1], their mesh constant is enclosed by [F8], and their arithmetic interval operations are sound by [A2].

1.2A2F1F4F5F9algebrainduction

For a Miller candidate, [F1] requires $x > 0$ and $N = n + q > n$ , and obtains $J_{0}, J_{1}, J_{n}, J_{N + 1}$ from successful $SeriesJ$ calls. Their intervals contain these exact values by [F4] and [A2]. Starting from $D_{0} = - J_{1}, D_{1} = J_{0}$ , induction through the finite recurrence [F9] and [A2] encloses every $D_{j}$ required by the error formula, including $D_{n}, D_{s}, D_{N + 1}$ . The prescribed terminal singletons and backward recurrence similarly enclose every exact $u_{j}$ . The procedure divides only after the interval for $D_{N + 1}$ excludes zero, so the resulting interval contains $q_{M} = - J_{N + 1} / D_{N + 1}$ . It also requires the intervals for $u_{s}$ , $J_{s}$ and $J_{s} + q_{M} D_{s}$ to exclude zero. Thus the exact denominators in [F5] are nonzero, and [A2] encloses both ${\hat{J}}_{n} = J_{s} u_{n} / u_{s}$ and its exact error $E_{M}$ from [F5]. Their interval difference contains ${\hat{J}}_{n} - E_{M} = J_{n}$ . Repeated occurrences of the same enclosed values may widen this difference but preserve containment; unavailable calls or failed guards discard the candidate.

2.1F1step 1.1step 1.2

Every candidate used by the procedure therefore contains the same exact requested value. Any nonempty intersection of candidates also contains that value.

3.1A1F1F3step 2.1

The algorithm reports success only after the containing interval passes the absolute-radius test and, when reported, the zero-excluding relative test in [F3]. Otherwise it returns an inconclusive or range status under finite caps. Thus the success claims are sound and do not rely on a limit as the Miller terminal index grows.

4.1givenA1step 3.1algebra∎

The stage and candidate loops are finite, every series and recurrence uses at most its stated finite index, and each elementary-range call has a finite DAG, format, and truncation index. Hence every capped execution terminates.

Depends on

Used by

Cited to discharge well-definedness by Finite certified evaluation of integer-order Bessel functions.

Dependency tree · two levels

39 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, §10.9, integral representations (standard reference, not scraped)
DLMF, §10.6, recurrence relations and derivatives (standard reference, not scraped)
DLMF, §10.2, Bessel functions of the first kind (standard reference, not scraped)
DLMF, §§10.2, 10.6, 10.9, 10.25, and 10.74(iii) (standard reference, not scraped)
N. M. Temme, “Numerical aspects of special functions,” Acta Numerica 17 (2008), §§2 and 4 (standard reference, not scraped)