Pipeline-generated

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.

✓ 3 results · all verified · 0 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 3 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Interval newton krawczyk and polynomial root isolation — Examples

1 · Prerequisites

2 · Summary

These examples show why sign-change searches miss a double root, how an exact mass-action balance can be certified inside a positive concentration box, and how a derivative bound certifies a unique event time. Each calculation uses the theorem whose hypotheses it checks; failure or unresolved output is not treated as root absence.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

A double polynomial root has no sign change

Example

For $p (x) = (x - 1)^{2} = x^{2} - 2 x + 1$ , the values at $0$ and $2$ are both positive, so endpoint signs do not reveal its real root. The exact gcd decomposition labels the root $1$ with multiplicity $2$ . The exact dyadic Sturm algorithm returns the isolating interval $(- 3, 3)$ with multiplicity $2$ .

Facts & Assumptions

Given: $p (x) = x^{2} - 2 x + 1$ and the exact rational root-isolation procedure.

[F1]

The gcd decomposition places a root of multiplicity $k$ in the squarefree factor $q_{k}$ (Exact gcd squarefree decomposition preserves roots and multiplicities).

[F2]

For a squarefree polynomial with nonroot endpoints, the Sturm variation difference counts its distinct roots in the open interval (Sturm sign variation counts distinct real polynomial roots).

[F3]

The root-isolation algorithm returns exact isolating intervals labelled by multiplicity and terminates on every nonzero rational polynomial (Exact Sturm bisection isolates every distinct real root of a nonzero rational polynomial).

Verification

1.1givenF1algebra

Direct calculation gives $p^{'} (x) = 2 x - 2$ and $\gcd (p, p^{'}) = x - 1$ after monic normalization. Thus $q_{2} = x - 1$ and $q_{1} = 1$ in [F1], so $1$ is a double root. Also $p (0) = p (2) = 1 > 0$ , and $p (x) = (x - 1)^{2} \geq 0$ , so there is no sign change across the root.

2.1givenF2F3algebra∎

The squarefree part is $S = x - 1$ with Sturm sequence $(S, S^{'}) = (x - 1, 1)$ . At endpoints $- 3$ and $3$ , the sign lists are $(-, +)$ and $(+, +)$ , so $V (- 3) - V (3) = 1 - 0 = 1$ by [F2]. The coefficient height of $S$ is $1$ , hence the algorithm starts on $(- 3, 3)$ ; its single Sturm count is one and the factor count assigns multiplicity $2$ . By [F3], this is a complete isolating record.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

A validated mass-action chemical equilibrium root

Example

Consider the reversible reaction $2 A ⇌ B$ with equilibrium constant $1$ and conserved amount $[A] + 2 [B] = 1$ . Writing $a = [A]$ , the mass-action equilibrium relation is $[B] = a^{2}$ , so the reduced residual is $f (a) = 2 a^{2} + a - 1$ . The dyadic box $X = [3 / 8, 5 / 8]$ certifies one positive equilibrium with $a = 1 / 2$ and $[B] = 1 / 4$ .

Facts & Assumptions

Given: The stated mass-action relation, conservation law, residual $f (a) = 2 a^{2} + a - 1$ , and box $X = [3 / 8, 5 / 8]$ .

[F1]

The scalar procedure forms an outward interval Newton image from an enclosure of $f (m)$ and an interval enclosure of $f^{'} (X)$ ; strict inclusion returns a unique-root status (Finite-budget scalar interval Newton root certification).

[F2]

If $0 \notin f^{'} (X)$ and the interval Newton image lies in $int X$ , then $f$ has exactly one root in $X$ (Scalar interval Newton exclusion and strict inclusion certificates).

[F3]

Finite real interval arithmetic encloses exact additions, multiplications, divisions away from zero, and squares (Finite real interval operations enclose their exact values).

[F4]

The derivative on a real interval is the ordinary difference-quotient limit (Continuity and derivative on a real interval).

Verification

1.1givenalgebra

The conservation law and $[B] = a^{2}$ reduce to $f (a) = a + 2 a^{2} - 1 = 0$ . At $a = 1 / 2$ , $[B] = 1 / 4$ , so $[B] = a^{2}$ and $a + 2 [B] = 1 / 2 + 1 / 2 = 1$ ; both concentrations are positive.

1.2givenF3F4algebra

Natural interval evaluation gives $E_{f} (X) = 2 [3 / 8, 5 / 8]^{2} + [3 / 8, 5 / 8] - 1 = [- 11 / 32, 13 / 32]$ , which contains zero. The difference quotient gives $f^{'} (a) = \lim_{h \to 0} (4 a h + 2 h^{2} + h) / h = 4 a + 1$ . The midpoint of $X$ is $m = 1 / 2$ , with $f (m) = 0$ and $f^{'} (X) = 4 [3 / 8, 5 / 8] + 1 = [5 / 2, 7 / 2]$ , which excludes zero.

2.1step 1.1step 1.2F1F2F3∎

The interval Newton image is $N = m - [0, 0] / [5 / 2, 7 / 2] = {1 / 2}$ by exact interval arithmetic [F3]. Since ${1 / 2} \subset (3 / 8, 5 / 8)$ , the algorithm returns "unique-root" by [F1], and [F2] proves that this is the only root in the box. The box therefore certifies the stated positive equilibrium.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

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]$ .