ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Simple unit-circle roots give bounded oscillatory modes

Example

The consistent three-step formula with $ρ (ζ) = (ζ - 1) (ζ^{2} + 1)$ and $σ (ζ) = 2$ has simple roots $1, i, - i$ on the unit circle. Its homogeneous modes include $1, i^{n}, (- i)^{n}$ ; their real and imaginary parts are bounded periodic real solutions.

Facts & Assumptions

Given: The root-condition and order conventions in Linear multistep methods, consistency, order, and the root condition.

[F1]

Taylor moment conditions characterize the order of a linear multistep method characterizes consistency by the first two moment conditions.

[L1]

The root condition is equivalent to bounded powers of the multistep companion matrix proves that the root condition implies bounded companion powers.

[F2]

$\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ gives Euler's formula and $∣ \exp (i y) ∣ = 1$ for real $y$ .

[F3]

$\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential gives $\exp (z + w) = \exp z \exp w$ .

[F4]

Quarter-turn values and shifts by pi/2 and pi gives $\cos (π / 2) = 0$ and $\sin (π / 2) = 1$ .

[F5]

The complex numbers as $R [x] / (x^{2} + 1)$ , with the real embedding and imaginary unit $i$ defines $i$ by $i^{2} = - 1$ .

Verification

1.1F1F5algebra

Expanding gives $ρ (ζ) = ζ^{3} - ζ^{2} + ζ - 1$ . Thus $ρ (1) = 0$ , $ρ^{'} (1) = 2 = σ (1)$ , and [F1] proves consistency. Since $i^{2} = - 1$ by [F5], the factorization displays three distinct roots $1, i, - i$ , all of modulus one, so the root condition holds.

1.2F2F3F4algebra

By [F2] and [F4], $i = \exp (i π / 2)$ and $∣ i ∣ = ∣ - i ∣ = 1$ . Repeated use of [F3] gives $i^{n} = \exp (i n π / 2)$ , so $i^{n}$ has modulus one by [F2]; also $(- i)^{n} = (- 1)^{n} i^{n}$ has modulus one. Each is a recurrence mode because substituting $Y_{n} = λ^{n}$ multiplies the homogeneous recurrence by $ρ (λ)$ .

2.1L1step 1.1step 1.2∎

Apply [L1] to the root condition in step 1.1. The full homogeneous companion recurrence is bounded, including these periodic modes; no decay of unit-circle modes is asserted.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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