TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

Separated Schur–Parlett blocks reconstruct the analytic matrix function

Statement

If Finite Schur–Parlett recurrence with block merging and inconclusive statuses returns parlett-success for an exact Schur pair $A = Q T Q^{*}$ , then its returned factored matrix $Q F Q^{*}$ equals the analytic primary matrix function $f (A)$ . This is a conditional exact correctness result, not a stability bound for the rounded Schur candidate generation.

Facts & Assumptions

Given: A successful algorithm output, its exact Schur certificate, its diagonal Jordan evaluations, and its exact Sylvester block solves.

[F1]

Success requires exact identities $Q^{*} Q = I$ and $A = Q T Q^{*}$ , zero blocks $F_{i j}$ for $i > j$ , exact-status diagonal Jordan evaluations, and the block Parlett Sylvester equations (Finite Schur–Parlett recurrence with block merging and inconclusive statuses). The diagonal outputs satisfy $F_{i i} = f (T_{i i})$ by A verified Jordan evaluation returns the primary matrix function.

[F2]

The analytic primary function is a polynomial in its matrix, commutes with it, and preserves block upper triangular form with diagonal blocks $f (T_{i i})$ (Jordan, contour, similarity, and normal-functional-calculus formulas agree).

[F3]

Every successful Bartels–Stewart solve has a unique exact solution because its verified local pivot maps are invertible and its finite block traversal solves the full operator (Finite Bartels–Stewart statuses and successful-pivot uniqueness).

[F4]

A successful Bartels–Stewart substitution returns the exact local Sylvester solution (Successful certified Bartels-Stewart substitution returns the exact Sylvester solution).

Proof

1.1F1F2

Let $G = f (T)$ . By [F2], $G$ is block upper triangular with diagonal blocks $G_{i i} = f (T_{i i})$ . By [F1], the algorithm's diagonal blocks equal these blocks, and both $F$ and $G$ have zero blocks below the diagonal.

1.2F1F2algebra

Expanding $G T = T G$ in block $(i, j)$ for $i < j$ gives $T_{i i} G_{i j} - G_{i j} T_{j j} = G_{i i} T_{i j} - T_{i j} G_{j j} + \sum_{i < k < j} (G_{i k} T_{k j} - T_{i k} G_{k j}) .$ This is the recurrence solved by the algorithm.

2.1F1F3F4step 1.1step 1.2induction

Induct on the block distance $j - i$ . At distance one, the recurrence right-hand side in step 1.2 uses only the matching diagonal blocks from step 1.1. The successful local solve from [F4] returns its exact solution, which is unique by the successful-pivot conclusion [F3]; hence $F_{i j} = G_{i j}$ . At larger distance, all shorter blocks on the right-hand side already agree by induction, so the same uniqueness argument gives $F_{i j} = G_{i j}$ .

3.1F1F2step 1.1step 2.1∎

Steps 1.1 and 2.1 show $F = G = f (T)$ . By [F1], $A = Q T Q^{*}$ with $Q$ unitary; similarity invariance in [F2] gives $Q F Q^{*} = Q f (T) Q^{*} = f (A)$ , which is the returned factored value.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

27 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

Jan Zur, Matrix Functions, TU Berlin full lecture notes (standard reference, not scraped)
Philip I. Davies and Nicholas J. Higham, A Schur–Parlett Algorithm for Computing Matrix Functions (standard reference, not scraped)