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 and finite termination of smooth-function root isolation
Statement
For valid interval range and derivative enclosures on every queried box, each finite run of Finite-budget interval isolation for smooth scalar roots terminates. Every excluded box contains no root, every certified box contains exactly one root, and every root in the initial interval belongs to a certified box or an unresolved box. A strict interval-Newton inclusion places its root in the interior of the scalar call's box. If the scalar procedure certifies after contraction to an exact singleton, the smooth isolator records the original processed interval, whose root may be at an endpoint. An inconclusive status, including a width or box-budget stop, gives no all-roots conclusion.
Facts & Assumptions
Given: A function on an open interval, a compact dyadic initial interval, valid range and derivative enclosures, a positive minimum width, and a finite box budget.
The isolator processes a finite queue, calls the scalar interval Newton procedure, bisects unresolved boxes, and returns every queued box as unresolved when the budget is exhausted (Finite-budget interval isolation for smooth scalar roots).
A scalar interval Newton "root-free" status excludes roots, and a "unique-root" status contains exactly one root (Scalar interval Newton exclusion and strict inclusion certificates).
Proof
Initially the queue contains the initial interval. Each processed box is either certified root-free, certified to contain one root, recorded unresolved at the width threshold, or replaced by its two closed halves. Those halves cover their parent, so by induction every root not already certified remains in a queued or unresolved interval.
Each processing removes one queued box and adds at most two; after at most processed boxes the queue is finite with at most entries. The algorithm then records the entire remainder as unresolved, so it terminates for every finite budget.
By [F2], no root lies in an excluded box and each certified box has exactly one root. The queue-coverage invariant from step 1.1 places every other root in an unresolved box. Strict-inclusion certificates put their roots in the interiors of the scalar call's boxes; if the scalar procedure certifies after contraction to a singleton, the recorded smooth box is the original processed interval and can contain the root at an endpoint. Therefore unresolved output blocks any claim that all roots have been isolated; it is not evidence of absence.
Depends on
Used by
- An event root with derivative bounded away from zero Example
- The hybrid event locator returns sound certificates or explicit failure within its budget Theorem
Cited to discharge well-definedness by Finite-budget interval isolation for smooth scalar roots.
Dependency tree · two levels
10 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
- Siegfried M. Rump, Verification methods: Rigorous results using floating-point arithmetic, Acta Numerica 19 (2010), §§6.2 and 13.1 (standard reference, not scraped)
- R. Baker Kearfott, Interval Computations: Introduction, Uses, and Resources, §2 (standard reference, not scraped)