Alphabeta Math
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 Airy enclosures

Statement

Whenever Finite certified Airy power-series evaluation returns success, its interval or rectangle contains the requested Ai⁡(z) or Bi⁡(z) and passes the requested absolute-radius test. Any relative certificate is valid only when the enclosure excludes zero. No success guarantee is made for every input or finite cap. Every execution with finite caps terminates.

Facts & Assumptions

Given: A successful return of Finite certified Airy power-series evaluation using a sound outward interval backend.

[A1]

Finite certified evaluation of Gamma and a continued log-Gamma branch supplies each finite Gamma call; Soundness of finite Gamma and log-Gamma enclosures says every successful call encloses the Gamma range on its dyadic input rectangle.

[A2]

Certified range evaluation for elementary real and complex functions supplies the finite real range calls for powers of 3; their finite outputs are sound by Certified real elementary-function evaluations enclose their ranges.

[A3]

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]

Certified special-function enclosure result: the success radius test and zero-exclusion rule have the stated absolute and relative meanings.

[F2]

Airy coefficient recurrence and geometric tail bounds: each nonzero Airy residue-class tail is bounded by its first omitted term divided by 1−q when all later ratios are at most q<1.

[F3]

Finite certified Airy power-series evaluation: the procedure encloses the two partial sums, adds the two residue-class tail bounds, and uses certified Gamma initial constants.

Proof

1.1A1A2A3F3

The initial coefficients used by the procedure enclose the exact Airy initial values by [F3], with the Gamma calls sound by [A1] and the powers of 3 sound by [A2]. Arithmetic on these intervals is sound by [A3]. The series definition and recurrence determine all later coefficients, so the resulting partial sums enclose their exact finite series sums.

2.1A3F2F3step 1.1

By [F2], each nonzero omitted class tail lies within its computed absolute tail bound; the third class is zero because its initial coefficient is zero and the recurrence preserves zero. Therefore the exact Airy value lies in the partial-sum enclosure enlarged by the sum of the two tail bounds.

3.1A1A2F1F3step 2.1

The algorithm reports success only when that containing rectangle passes the requested radius test, and its relative flag obeys [F1]. If its finite caps do not allow that test, the result is inconclusive; no claim of universal success is made.

4.1givenA1A2step 3.1algebra∎

The stage loop is finite; each Gamma and elementary-range subcall has finite caps and truncation index, and the residue-class sums have at most the capped number of terms. Thus every capped execution terminates.

Depends on

Used by

Cited to discharge well-definedness by Finite certified Airy power-series evaluation.

Dependency tree · two levels

32 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