TheoremStatement: 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.

Phi recurrence and augmented-matrix action identities

Statement

For every integer $k \geq 0$ , scalar $z \in C$ , and square matrix $X \in M_{n} (C)$ with $n \geq 0$ , the series-defined functions of The phi-function family by everywhere-convergent series satisfy

$φ_{k} (z) = \frac{1}{k!} + z φ_{k + 1} (z), φ_{k} (X) = \frac{1}{k!} I_{n} + X φ_{k + 1} (X) .$

For $k \geq 1$ and $w \in C^{n}$ , let $J_{k} \in M_{k} (C)$ have ones on the superdiagonal and zeros elsewhere, and let $e_{1}, e_{k} \in C^{k}$ be the first and last coordinate vectors. Define $B_{k} (X, w) : = [\begin{array}{cc} X & w e_{1}^{*} \\ 0 & J_{k} \end{array}]$ . Then the first $n$ entries of $e^{B_{k} (X, w)} [\begin{array}{c} 0 \\ e_{k} \end{array}]$ equal $φ_{k} (X) w$ . The identity is valid at $X = 0$ and requires no division by $X$ or by a scalar argument.

Facts & Assumptions

Given: $k \geq 0$ , $z \in C$ , $X \in M_{n} (C)$ with $n \geq 0$ , and $w \in C^{n}$ when $k \geq 1$ .

[F1]

The phi-function family by everywhere-convergent series: $φ_{k} (z) = \sum_{j \geq 0} z^{j} / (j + k)!$ and $φ_{k} (X) = \sum_{j \geq 0} X^{j} / (j + k)!$ .

[F2]

The scalar and matrix phi series converge absolutely: these scalar and matrix series converge absolutely, so their tails may be reindexed and their matrix-exponential blocks may be read termwise.

Proof

technique · direct

1.1F1F2algebra

Absolute convergence in [F2] permits an index shift: $z φ_{k + 1} (z) = \sum_{j \geq 0} z^{j + 1} / (j + k + 1)! = \sum_{r \geq 1} z^{r} / (r + k)! = φ_{k} (z) - 1 / k!$ . Rearranging proves the scalar recurrence, including $z = 0$ .

1.2F1F2algebra

For $n = 0$ , every matrix term is the unique empty matrix by [F1], so the matrix recurrence is the equality of that matrix with itself. For $n \geq 1$ , the same index shift is valid in operator norm by [F2]; left multiplication by $X$ sends the $(j + k + 1)!$ denominator term to $X^{j + 1} / (j + k + 1)!$ . Thus $X φ_{k + 1} (X) = φ_{k} (X) - I_{n} / k!$ , proving the matrix recurrence.

1.3givenalgebra

For $n \geq 1$ , in $B_{k} (X, w)$ , a block-product path from the first block row to the last column of the last block must move through the $w e_{1}^{*}$ block and then through all $k - 1$ superdiagonal entries of $J_{k}$ . It uses exactly $k$ block transitions; any remaining factors can only be copies of $X$ before that first transition. Hence the last column of the top-right block of $B_{k}^{r}$ is zero for $r < k$ , and is $X^{r - k} w$ for $r \geq k$ .

2.1step 1.3F1F2algebra∎

For $n \geq 1$ , by [F2] with $k = 0$ , $e^{B_{k}} = φ_{0} (B_{k}) = \sum_{r \geq 0} B_{k}^{r} / r!$ . By step 1.3, the last column of its top-right block is $\sum_{r \geq k} X^{r - k} w / r! = \sum_{j \geq 0} X^{j} w / (j + k)! = φ_{k} (X) w$ . This is exactly the first $n$ entries obtained by applying $e^{B_{k}}$ to the last coordinate vector. When $n = 0$ , $w$ is the unique vector in $C^{0}$ and $B_{k} (X, w) = J_{k}$ ; the first zero entries of $e^{J_{k}} e_{k}$ and $φ_{k} (X) w$ are both the empty vector. Thus the augmented identity also holds in that case.

Depends on

Used by

Dependency tree · two levels

13 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

Awad H. Al-Mohy and Nicholas J. Higham, Computing the action of the matrix exponential, with an application to exponential integrators (standard reference, not scraped)
Jitse Niesen and Will M. Wright, A Krylov subspace algorithm for evaluating the phi-functions appearing in exponential integrators (standard reference, not scraped)