ExampleConstruction: AI-generatedVerification: 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.

An event root with derivative bounded away from zero

Example

Let an event surface be $g (t) = t^{2} - 2$ on the time interval $[1, 2]$ . Its derivative is bounded below by $2$ , and a strict interval Newton inclusion certifies a unique event time in the box $[1, 2]$ .

Facts & Assumptions

Given: $g (t) = t^{2} - 2$ on $[1, 2]$ and interval Newton evaluation with exact dyadic endpoints.

[F1]

The smooth isolator calls the scalar interval Newton procedure on each box and retains unresolved boxes when a certificate fails or a budget is exhausted (Finite-budget interval isolation for smooth scalar roots).

[F2]

A strict scalar interval Newton inclusion proves existence and uniqueness in the box (Scalar interval Newton exclusion and strict inclusion certificates).

[F3]

Finite real interval operations enclose exact values (Finite real interval operations enclose their exact values).

[F4]

A real derivative is the limit of its difference quotients (Continuity and derivative on a real interval).

Verification

1.1givenF3F4algebra

Natural interval evaluation gives $E_{g} ([1, 2]) = [1, 4] - 2 = [- 1, 2]$ , which contains zero. For $t \in [1, 2]$ , the difference quotient gives $g^{'} (t) = 2 t \in [2, 4]$ , so the derivative enclosure excludes zero with margin $2$ . At the midpoint $m = 3 / 2$ , $g (m) = 1 / 4$ .

2.1step 1.1F3algebra

The interval quotient is $[1 / 4] / [2, 4] = [1 / 16, 1 / 8]$ , hence the Newton image is $N = 3 / 2 - [1 / 16, 1 / 8] = [11 / 8, 23 / 16] \subset (1, 2)$ .

3.1step 2.1F1F2∎

With minimum width $1 / 2$ and box budget $1$ , the smooth isolator makes one scalar call on $[1, 2]$ . The strict inclusion certifies exactly one root in this box by [F2], so the call returns "unique-root" and the isolator returns it as a certified event-time box. No conclusion is drawn about roots outside $[1, 2]$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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