PropositionStatement: Literature-sourcedProof: 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.

RKC stability polynomials and certified negative-real intervals

Statement

On the scalar test equation $y^{'} = λ y$ , write $z = h λ$ and let $R (z)$ be the factor by which a successful method step multiplies $y$ .

For first-order RKC with $s \geq 1$ stages, $R_{1, s} (z) = T_{s} (1 + z / s^{2}) .$ It has degree $s$ , satisfies $R_{1, s} (0) = R_{1, s}^{'} (0) = 1$ , and its real absolute stability set ${z \in R : ∣ R_{1, s} (z) ∣ \leq 1}$ is exactly $[- 2 s^{2}, 0]$ .

For second-order RKC with $s \geq 2$ stages, both the linear algorithm and the scalar-linear specialization of the nonlinear algorithm have $R_{2, s} (z) = a_{s} + b_{s} T_{s} (1 + w_{1} z), w_{1} = \frac{3}{s^{2} - 1}, b_{s} = \frac{s^{2} - 1}{3 s^{2}}, a_{s} = 1 - b_{s} .$ This polynomial has degree $s$ and satisfies $R_{2, s} (0) = R_{2, s}^{'} (0) = R_{2, s}^{''} (0) = 1$ . It is absolutely stable on the real interval $[- 2 (s^{2} - 1) / 3, 0]$ ; this is a certified interval and is not claimed to be the maximal real stability set.

Let $d \geq 1$ , let $A$ be a self-adjoint endomorphism of $R^{d}$ with its Euclidean inner product, and assume $⟨ A v, v ⟩ \leq 0$ for every $v$ . Let $ρ = \max_{i} (- λ_{i})$ , where $λ_{i}$ are the eigenvalues of $A$ . If $h ρ \leq 2 s^{2}$ , first-order RKC is nonexpansive in the Euclidean norm; if $h ρ \leq 2 (s^{2} - 1) / 3$ , linear second-order RKC is nonexpansive. The same linear contraction statement holds for the nonlinear RKC method when applied to $f (y) = A y$ . No corresponding claim is made for nonnormal matrices.

Facts & Assumptions

Given: The stated RKC recurrences, $s \geq 1$ for first-order RKC, $s \geq 2$ for second-order RKC, and the self-adjoint nonpositive operator hypotheses in the matrix clause.

[F1]

First-order stabilized explicit Runge–Kutta–Chebyshev step: $Y_{0} = y$ , $Y_{1} = (I + h A / s^{2}) Y_{0}$ , and $Y_{j} = 2 (I + h A / s^{2}) Y_{j - 1} - Y_{j - 2}$ for $j \geq 2$ when $f (y) = A y$ .

[F2]

Second-order linear stabilized Runge–Kutta–Chebyshev step: $V_{0} = y$ , $V_{1} = (I + w_{1} h A) V_{0}$ , $V_{j} = 2 (I + w_{1} h A) V_{j - 1} - V_{j - 2}$ , and the output is $a_{s} V_{0} + b_{s} V_{s}$ .

[F3]

Second-order nonlinear stabilized Runge–Kutta–Chebyshev step: the nonlinear stage recurrence uses $b_{0} = b_{1} = b_{2} = 1 / 4$ , $a_{j} = 1 - b_{j}$ , and the displayed $μ_{j}, ν_{j}, m_{j}, g_{j}$ coefficients.

[F4]

Chebyshev polynomials of the first and second kinds by their three-term recurrences: $T_{n + 2} (x) = 2 x T_{n + 1} (x) - T_{n} (x)$ and $U_{n + 2} (x) = 2 x U_{n + 1} (x) - U_{n} (x)$ .

[F5]

Chebyshev bounds and endpoint derivatives used by stabilized Runge–Kutta methods: $∣ T_{n} (x) ∣ \leq 1$ on $[- 1, 1]$ , $∣ T_{n} (x) ∣ > 1$ for $∣ x ∣ > 1$ when $n \geq 1$ , the degrees/leading coefficients are $n, 2^{n - 1}$ for $T_{n}$ , and $T_{s}^{'} (1) = s^{2}$ , $T_{s}^{''} (1) = s^{2} (s^{2} - 1) / 3$ .

[F6]

Polynomial evaluation at an endomorphism: $p (T) = \sum_{k} a_{k} T^{k}$ : for a finite polynomial $p (x) = \sum_{k} a_{k} x^{k}$ , $p (A) = \sum_{k} a_{k} A^{k}$ with $A^{0} = I$ .

[F7]

Self-adjoint and normal endomorphisms of a finite-dimensional real or complex inner product space: self-adjoint means $A^{*} = A$ on the stated real inner-product space.

[F8]

Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis: a self-adjoint endomorphism on a finite-dimensional real inner-product space has an orthonormal eigenbasis.

[F9]

Real and complex inner-product spaces and their induced length, Orthonormal families, complete orthonormal systems and Hilbert bases, and The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : the Euclidean inner product is a real inner product; in an orthonormal basis, squared length is the sum of squared coordinates and $∥ v ∥_{2}^{2} = \sum_{i} v_{i}^{2}$ .

[F10]

The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ and Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ : a differentiable polynomial composed with an affine function obeys the chain rule; products and sums differentiate by their usual rules.

[A1]

$A$ is self-adjoint and $⟨ A v, v ⟩ \leq 0$ for every $v$ ; $h > 0$ and the stated spectral-radius inequality holds in the applicable branch.

Proof

1.1F1F4F5F6inductionalgebra

For $f (y) = A y$ , put $X = I + h A / s^{2}$ in [F1]. The Chebyshev recurrence [F4] and the definition of polynomial evaluation [F6] give $Y_{j} = T_{j} (X) y$ by induction from $T_{0} (X) y = y$ and $T_{1} (X) y = X y$ . Hence the output factor is $R_{1, s} (z) = T_{s} (1 + z / s^{2})$ . Its degree is $s$ because [F5] gives nonzero leading coefficient $2^{s - 1}$ and the affine argument has nonzero slope.

1.2F2F3F4F5inductionalgebra

In [F3], specialize to $f (y) = λ y$ . Define the scalar polynomial $P_{j}$ by $Y_{j} = P_{j} (z) y$ for every initial scalar $y$ ; the linear recurrence makes this definition valid even when $y = 0$ . Then $P_{0} = 1$ , $P_{1} = 1 + b_{1} w_{1} z$ , and for $j \geq 2$ , $P_{j} = (1 - μ_{j} - ν_{j}) + μ_{j} P_{j - 1} + ν_{j} P_{j - 2} + m_{j} z P_{j - 1} + g_{j} z .$ Set $x = 1 + w_{1} z$ . The base values satisfy $P_{0} = a_{0} + b_{0} T_{0} (x)$ and $P_{1} = a_{1} + b_{1} T_{1} (x)$ . If $P_{j - 1} = a_{j - 1} + b_{j - 1} T_{j - 1} (x)$ and $P_{j - 2} = a_{j - 2} + b_{j - 2} T_{j - 2} (x)$ , the coefficient of $T_{j - 1}$ is $μ_{j} b_{j - 1} + m_{j} z b_{j - 1} = 2 b_{j} (1 + w_{1} z) = 2 b_{j} x$ , and the coefficient of $T_{j - 2}$ is $ν_{j} b_{j - 2} = - b_{j}$ . The constant part is $1 - μ_{j} - ν_{j} + μ_{j} a_{j - 1} + ν_{j} a_{j - 2} + m_{j} z a_{j - 1} + g_{j} z = 1 - μ_{j} b_{j - 1} - ν_{j} b_{j - 2} + z (m_{j} a_{j - 1} + g_{j}) = 1 - b_{j} = a_{j},$ because $g_{j} = - a_{j - 1} m_{j}$ , $μ_{j} b_{j - 1} = 2 b_{j}$ , and $ν_{j} b_{j - 2} = - b_{j}$ . Thus $P_{j} = a_{j} + b_{j} T_{j} (x)$ by [F4]. The same coefficient induction with $z$ replaced by $h A$ proves that the nonlinear recurrence specialized to $f (v) = A v$ has update $a_{s} I + b_{s} T_{s} (I + w_{1} h A)$ . The linear algorithm [F2] has that same shifted-Chebyshev recurrence and final weights, so its final factor is the same $R_{2, s}$ . The degree is $s$ , since $b_{s} > 0$ , $w_{1} > 0$ , and [F5] gives degree $s$ with nonzero leading coefficient.

2.1F5F10step 1.1step 1.2algebra

By [F5], $T_{s} (1) = 1$ , $T_{s}^{'} (1) = s^{2}$ , and $T_{s}^{''} (1) = s^{2} (s^{2} - 1) / 3$ . The scalar chain rule and product rule [F10] applied to the polynomials in steps 1.1–1.2 therefore give $R_{1, s} (0) = 1$ and $R_{1, s}^{'} (0) = T_{s}^{'} (1) / s^{2} = 1$ . For second-order RKC, $a_{s} + b_{s} = 1$ , $b_{s} w_{1} s^{2} = 1$ , and $b_{s} w_{1}^{2} T_{s}^{''} (1) = \frac{s^{2} - 1}{3 s^{2}} \frac{9}{(s^{2} - 1)^{2}} \frac{s^{2} (s^{2} - 1)}{3} = 1.$ Differentiating the polynomial in step 1.2 gives the stated values of $R_{2, s} (0)$ , $R_{2, s}^{'} (0)$ , and $R_{2, s}^{''} (0)$ .

2.2F5step 1.1step 1.2algebra

For first-order RKC, $∣ R_{1, s} (z) ∣ \leq 1$ exactly when $x = 1 + z / s^{2}$ lies in $[- 1, 1]$ , by [F5]; solving these two inequalities gives $- 2 s^{2} \leq z \leq 0$ . For second-order RKC, $b_{s} > 0$ and $a_{s} = 1 - b_{s} > 0$ for $s \geq 2$ . If $- 2 / w_{1} \leq z \leq 0$ , then $x = 1 + w_{1} z \in [- 1, 1]$ , so [F5] gives $∣ a_{s} + b_{s} T_{s} (x) ∣ \leq a_{s} + b_{s} ∣ T_{s} (x) ∣ \leq a_{s} + b_{s} = 1$ . Since $2 / w_{1} = 2 (s^{2} - 1) / 3$ , the claimed interval follows.

3.1A1F2F6F7F8F9step 1.2step 2.2algebra∎

By [F8], choose an orthonormal eigenbasis $e_{i}$ with $A e_{i} = λ_{i} e_{i}$ . The nonpositive premise [A1] gives $λ_{i} \leq 0$ by applying it to $e_{i}$ . For any vector $v = \sum_{i} α_{i} e_{i}$ , polynomial evaluation gives $R (h A) v = \sum_{i} α_{i} R (h λ_{i}) e_{i}$ . Under the first-order spectral bound, every $h λ_{i} \in [- 2 s^{2}, 0]$ , so step 2.2 gives $∣ R_{1, s} (h λ_{i}) ∣ \leq 1$ ; orthonormality then yields $∥ R_{1, s} (h A) v ∥^{2} = \sum_{i} α_{i}^{2} R_{1, s} (h λ_{i})^{2} \leq \sum_{i} α_{i}^{2} = ∥ v ∥^{2}$ . Under the second-order spectral bound, the same calculation uses the interval from step 2.2 for $R_{2, s}$ . The scalar specialization in step 1.2 shows it also applies to nonlinear RKC on this linear field.

Remarks

The matrix conclusion uses an orthonormal eigenbasis and therefore does not follow from eigenvalue inclusion alone for a nonnormal matrix. For RKC2, the interval proved above is a guaranteed stability interval; the statement does not claim that it is the largest real interval in the absolute stability set.

Depends on

Used by

Dependency tree · two levels

68 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

Ibrahim Almuslimani and Gilles Vilmart, Explicit Stabilized Integrators for Stiff Optimal Control Problems, §§2.2.1–2.2.2 (standard reference, not scraped)
B.P. Sommeijer, L.F. Shampine, and J.G. Verwer, RKC: An explicit solver for parabolic PDEs, §2 (standard reference, not scraped)