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 · 1 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 2 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Matrix exponential and phi function actions — Examples

1 · Prerequisites

2 · Summary

The examples verify the phi-one augmented action at zero without a removable-singularity quotient, show how a one-vector Arnoldi projection can miss the slow mode of a stiff diagonal matrix, and compute an exact transient-growth example with a valid logarithmic-norm residual certificate. Their calculations use exact arithmetic; the theorem's separate finite-precision terms remain conditional on certified relation and reduced-action data.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

The value phi_1(0) is obtained directly from its series

Statement

For the zero $1 \times 1$ matrix, verify directly that $φ_{1} (0) = 1$ and that the augmented exponential returns this value without evaluating $(e^{z} - 1) / z$ .

Facts & Assumptions

Given: $X = [0] \in M_{1} (C)$ , $w = [1] \in C$ , and $k = 1$ .

[F1]

The phi-function family by everywhere-convergent series: $φ_{1} (X) = \sum_{j \geq 0} X^{j} / (j + 1)!$ , with $X^{0} = I_{n}$ .

[F2]

Phi recurrence and augmented-matrix action identities: the first coordinate of $e^{B_{1} (X, w)} (0, 1)^{T}$ is $φ_{1} (X) w$ , with no division by $X$ or a scalar.

Proof

1.1givenF1algebra

Since $X^{0} = [1]$ and $X^{j} = [0]$ for every $j \geq 1$ , the series in [F1] has only the term $1 / 1! = 1$ nonzero. Hence $φ_{1} (X) = [1]$ .

2.1givenstep 1.1F2algebra∎

Here $J_{1} = [0]$ and $B_{1} (X, w) = [\begin{array}{cc} 0 & 1 \\ 0 & 0 \end{array}] = : N$ , so $N^{2} = 0$ and $e^{N} = I + N$ . Therefore $e^{N} (0, 1)^{T} = (1, 1)^{T}$ ; [F2] identifies its first coordinate with $φ_{1} (X) w = 1$ . The quotient $(e^{z} - 1) / z$ is undefined at $z = 0$ , while the series and augmented action above are defined there.

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

A one-dimensional Arnoldi projection misses a slow mode of a stiff diagonal matrix

Statement

Let $A = diag (- 100, - 1)$ , $v = (1, 1)^{T}$ , $t = 1 / 10$ , and use one Arnoldi step ( $m = 1$ ). Compute the projected exponential action, compare it exactly with $e^{t A} v$ , and evaluate the residual-integral bound.

Facts & Assumptions

Given: The stated real diagonal matrix, nonzero starting vector, time, and exact-arithmetic Arnoldi run with $m = 1$ .

[F1]

The Arnoldi process for building an orthonormal basis of a Krylov subspace and Before breakdown, Arnoldi produces an orthonormal Krylov basis and a rectangular upper-Hessenberg factorization: the first Arnoldi vector is $q_{1} = v / ∥ v ∥_{2}$ , $H_{1} = q_{1}^{*} A q_{1}$ , and $A q_{1} = H_{1} q_{1} + h_{2, 1} q_{2}$ when the residual is nonzero.

[F2]

Arnoldi projection for exponential and phi-function actions: for $k = 0$ , the exact projected action is $∥ v ∥_{2} V_{1} e^{t H_{1}} e_{1}$ .

[F3]

Arnoldi action error is the semigroup-weighted residual integral: with exact Arnoldi and exact reduced action, zero initial mismatch, and $D = Ω = 0$ , the error is bounded by the semigroup-weighted integral of $h_{2, 1} ∣ e_{1}^{*} c (s) ∣$ , where $c (s) = e^{s H_{1}} ∥ v ∥_{2} e_{1}$ .

[F4]

The phi-function family by everywhere-convergent series: the diagonal exponential acts entrywise by the scalar exponential series.

[F5]

The Euclidean logarithmic norm of a complex matrix: $μ_{2} (A)$ is the largest eigenvalue of the Hermitian part $(A + A^{*}) / 2$ .

[F6]

The exponential is a continuous bijection from $R$ onto $(0, \infty)$ : the real exponential is injective on $R$ .

[F7]

$\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential: the complex exponential satisfies its addition law and agrees with the real exponential on real inputs.

[F8]

The exponential function is smooth and $(\exp)^{'} = \exp$ : $(\exp x)^{'} = \exp x$ for real $x$ .

[F9]

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)$ : differentiating a scalar exponential composed with a real affine map multiplies by that affine slope.

[F10]

If $f : [a, b] \to R^{m}$ is differentiable with integrable $f^{'}$ then $\int_{a}^{b} f^{'} = f (b) - f (a)$ ; and a bounded derivative makes $f$ Lipschitz: for a continuously differentiable real scalar function, its definite integral is the endpoint difference of an antiderivative.

[F11]

A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion: a continuous real-valued function on a nondegenerate closed bounded interval is Riemann integrable.

Proof

1.1givenF1algebra

We have $∥ v ∥_{2} = \sqrt{2}$ and $q_{1} = (1, 1)^{T} / \sqrt{2}$ . Thus $H_{1} = q_{1}^{*} A q_{1} = - 101 / 2$ . The Arnoldi residual is $A q_{1} - H_{1} q_{1} = (- 99, 99)^{T} / (2 \sqrt{2})$ , so its norm is $99 / 2$ and its normalization is $q_{2} = (- 1, 1)^{T} / \sqrt{2}$ .

2.1givenstep 1.1F2F4F6F7algebra

By [F2], the projected action is $\sqrt{2} q_{1} e^{- 101 / 20} = e^{- 101 / 20} (1, 1)^{T}$ . By [F4], the exact action is $(e^{- 10}, e^{- 1 / 10})^{T}$ . Its exact error vector is $(e^{- 10} - e^{- 101 / 20}, e^{- 1 / 10} - e^{- 101 / 20})^{T}$ , which is nonzero because [F7] identifies these real-argument complex exponentials with the real exponential, and $- 1 / 10 \neq - 101 / 20$ with injectivity from [F6].

3.1givenF3F5F7F8F9F10F11step 1.1algebra∎

The matrix is Hermitian with largest eigenvalue $- 1$ , so [F5] gives $μ_{2} (A) = - 1$ . Here $c (s) = \sqrt{2} e^{- 101 s / 2}$ and the initial mismatch $v - \sqrt{2} q_{1}$ is zero. By [F3], the certificate is $∥ e^{t A} v - V_{1} e^{t H_{1}} \sqrt{2} e_{1} ∥_{2} \leq \int_{0}^{1 / 10} e^{- (1 / 10 - s)} (99 / 2) \sqrt{2} e^{- 101 s / 2} d s$ . By the addition law [F7] its integrand is $e^{- 1 / 10} (99 / 2) \sqrt{2} e^{- 99 s / 2}$ , a continuous real function on $[0, 1 / 10]$ and hence integrable by [F11]. The antiderivative $- (2 / 99) e^{- 99 s / 2}$ follows from [F8] and [F9]; applying [F10] yields the bound $\sqrt{2} e^{- 1 / 10} (1 - e^{- 99 / 20})$ . Thus the slow component $e^{- 1 / 10}$ is missed by the one-dimensional projection even though the residual certificate applies.

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

A nonnormal action grows transiently while its Arnoldi residual certificate remains valid

Statement

Let $A = [\begin{array}{cc} - 1 & 3 \\ 0 & - 1 \end{array}]$ , $v = e_{2}$ , $t = 1$ , and use one exact Arnoldi step. Compute the exact action and projection, its residual certificate, and the logarithmic-norm growth bound.

Facts & Assumptions

Given: The stated real matrix, starting vector, time, and exact-arithmetic Arnoldi run with $m = 1$ .

[F1]

The Arnoldi process for building an orthonormal basis of a Krylov subspace and Before breakdown, Arnoldi produces an orthonormal Krylov basis and a rectangular upper-Hessenberg factorization: Arnoldi starts with $q_{1} = v / ∥ v ∥_{2}$ and represents $A q_{1} = H_{1} q_{1} + h_{2, 1} q_{2}$ for a nonzero residual.

[F2]

Arnoldi projection for exponential and phi-function actions: the exact one-step exponential projection is $∥ v ∥_{2} V_{1} e^{t H_{1}} e_{1}$ .

[F3]

The phi-function family by everywhere-convergent series and The scalar and matrix phi series converge absolutely: scalar and matrix exponentials are given by their absolutely convergent power series; in particular $e^{A} = \sum_{j \geq 0} A^{j} / j!$ and $\exp (- 1) = \sum_{j \geq 0} (- 1)^{j} / j!$ .

[F4]

The Euclidean logarithmic norm of a complex matrix and The logarithmic norm bounds forward and reverse matrix exponentials: $μ_{2} (A)$ is the largest eigenvalue of $(A + A^{*}) / 2$ , and $∥ e^{τ A} ∥_{2} \leq e^{τ μ_{2} (A)}$ for $τ \geq 0$ .

[F5]

Arnoldi action error is the semigroup-weighted residual integral: the exact action error is the initial mismatch term plus the oriented integral of $e^{(t - s) A} (A V - V H) c (s)$ ; its norm is bounded by the logarithmic-norm-weighted residual integral, with no added $D$ , $Ω$ , or reduced-action term when these are zero.

[F6]

The real exponential function and the number $e$ by a power series and The exponential series converges absolutely for every real argument: $e = \sum_{j \geq 0} 1 / j!$ .

[F7]

The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ : for every real $x$ , $\exp (x) > 0$ and $\exp (- x) = 1 / \exp (x)$ .

[F8]

$\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential: the complex exponential satisfies its addition law and agrees with the real exponential on real inputs.

[F9]

The exponential function is smooth and $(\exp)^{'} = \exp$ : $(\exp x)^{'} = \exp x$ for real $x$ .

[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)$ : differentiating an exponential composed with a real affine map multiplies by the affine slope.

[F11]

If $f : [a, b] \to R^{m}$ is differentiable with integrable $f^{'}$ then $\int_{a}^{b} f^{'} = f (b) - f (a)$ ; and a bounded derivative makes $f$ Lipschitz: for a continuously differentiable real scalar function, the definite integral equals the endpoint difference of an antiderivative.

[F12]

A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion: every continuous real-valued function on a nondegenerate closed bounded interval is Riemann integrable.

Proof

1.1givenF1F2F8algebra

With $q_{1} = e_{2}$ , $H_{1} = e_{2}^{*} A e_{2} = - 1$ and $A e_{2} - H_{1} e_{2} = 3 e_{1}$ , so $h_{2, 1} = 3$ and $q_{2} = e_{1}$ . Therefore [F2] gives the projection $e^{- 1} e_{2}$ , where [F8] identifies this scalar value with the real exponential.

2.1givenF3F6F7F8step 1.1algebrainduction

Write $A = - I + N$ , where $N = [\begin{array}{cc} 0 & 3 \\ 0 & 0 \end{array}]$ and $N^{2} = 0$ . For $j = 1$ , $A = (- 1) I + N$ ; if $A^{j} = (- 1)^{j} I + j (- 1)^{j - 1} N$ , multiplying by $- I + N$ and using $N^{2} = 0$ yields $A^{j + 1} = (- 1)^{j + 1} I + (j + 1) (- 1)^{j} N$ . Thus induction proves the formula for all $j \geq 1$ . Substituting into [F3] and using absolute convergence to reindex gives $e^{A} = \sum_{j \geq 0} A^{j} / j! = (\sum_{j \geq 0} (- 1)^{j} / j!) I + (\sum_{j \geq 1} (- 1)^{j - 1} / (j - 1)!) N = e^{- 1} (I + N)$ . By [F8], the scalar complex value at $- 1$ is the real $e^{- 1}$ , and [F7] gives $e^{- 1} = 1 / e$ . Thus $e^{A} e_{2} = e^{- 1} (3 e_{1} + e_{2})$ and the exact projection error is $3 / e$ . For every $j \geq 1$ , the $j - 1$ factors $2, \dots, j$ in $j!$ are at least $2$ , so $j! \geq 2^{j - 1}$ , strictly for $j \geq 3$ ; hence [F6] gives $e = 1 + \sum_{j \geq 1} 1 / j! < 1 + \sum_{j \geq 1} 2^{- (j - 1)} = 3 < \sqrt{10}$ . Positivity and reciprocity in [F7] now give $∥ e^{A} e_{2} ∥_{2} = \sqrt{10} / e > 1$ , so the action grows in norm from the unit initial vector.

3.1givenF4F5F8F9F10F11F12step 1.1algebra∎

The Hermitian part is $[\begin{array}{cc} - 1 & 3 / 2 \\ 3 / 2 & - 1 \end{array}]$ , with eigenvalues $1 / 2$ and $- 5 / 2$ , hence by [F4] $μ_{2} (A) = 1 / 2$ . The semigroup bound in [F4] is $∥ e^{τ A} ∥_{2} \leq e^{τ / 2}$ . In the residual estimate $c (s) = e^{- s}$ , so [F5] gives $∥ e^{A} e_{2} - e^{- 1} e_{2} ∥_{2} \leq \int_{0}^{1} 3 e^{(1 - s) / 2} e^{- s} d s$ . By [F8], the integrand is $3 e^{1 / 2} e^{- 3 s / 2}$ , which is continuous on $[0, 1]$ and integrable by [F12]. An antiderivative of $e^{- 3 s / 2}$ is $- (2 / 3) e^{- 3 s / 2}$ by [F9] and [F10]; [F11] then evaluates the bound as $2 e^{1 / 2} (1 - e^{- 3 / 2})$ . For the exact residual identity in [F5], $N e_{1} = 0$ gives $e^{(1 - s) A} e_{1} = e^{- (1 - s)} e_{1}$ . The addition law [F8] makes the residual integrand the constant vector $3 e^{- 1} e_{1}$ , whose coordinates are continuous and integrable by [F12]; [F11] gives $\int_{0}^{1} e^{(1 - s) A} (3 e^{- s} e_{1}) d s = (3 / e) e_{1}$ , consistent with the exact error. The certificate remains valid in this nonnormal case, while the positive logarithmic norm allows transient growth.

Matrix exponential and phi function actions — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

The value phi_1(0) is obtained directly from its series

Statement

Facts & Assumptions

Proof

A one-dimensional Arnoldi projection misses a slow mode of a stiff diagonal matrix

Statement

Facts & Assumptions

Proof

A nonnormal action grows transiently while its Arnoldi residual certificate remains valid

Statement

Facts & Assumptions

Proof

Sources