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.

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.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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