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 Functions and Scaling Squaring — Examples

1 · Prerequisites

2 · Summary

The examples compute a positive diagonal Gram matrix and its polar factors, show how a stable spectrum can coexist with a large transient norm for a nonnormal exponential, and locate the planar half-turn on the principal logarithm branch cut. Each calculation states the matrix identities and spectral facts it uses.

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 →

A positive diagonal Gram matrix gives a nontrivial polar factor

Example

For $A = (\begin{array}{cc} 0 & - 2 \\ 1 & 0 \end{array}),$ the Gram matrix is positive diagonal, its positive square root is nontrivial, and the polar isometry is a quarter-turn.

Facts & Assumptions

Given: The displayed real matrix $A$ .

[F1]

A nonnegative matrix has a unique nonnegative square root (A non-negative operator has a unique non-negative square root).

[F2]

The polar decomposition has positive factor $\sqrt{A^{*} A}$ and isometry factor $S$ with $A = S \sqrt{A^{*} A}$ (Every endomorphism has a polar decomposition T = SU with U non-negative and S an isometry on the orthogonal complement of ker T, and S is unique exactly when T is invertible).

Verification

1.1givenF1algebra

Direct multiplication gives $A^{*} A = (\begin{array}{cc} 1 & 0 \\ 0 & 4 \end{array})$ , and $H = (\begin{array}{cc} 1 & 0 \\ 0 & 2 \end{array})$ is positive with $H^{2} = A^{*} A$ . By [F1], $H$ is the unique nonnegative square root.

2.1F2step 1.1algebra∎

Put $S = (\begin{array}{cc} 0 & - 1 \\ 1 & 0 \end{array})$ . Then $S^{*} S = I$ and $S H = A$ , so [F2] identifies $S$ as the polar isometry and $H$ as its positive factor.

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

A stable-spectrum nonnormal exponential has a large transient norm

Example

Let $A = (\begin{array}{cc} - 1 & 10 \\ 0 & - 1 \end{array}) .$ Its eigenvalues have negative real part, but at time $t = 1$ the row-sum norm of $e^{A}$ is greater than one. Here the row-sum norm is $∥ M ∥_{r o w} = \max_{i} \sum_{j} ∣ M_{i j} ∣$ .

Facts & Assumptions

Given: The displayed matrix $A$ .

[F1]

The complex exponential is its power-series exponential and its primary matrix value is given by the Jordan-block formula (The complex exponential by its power series, Jordan, contour, similarity, and normal-functional-calculus formulas agree).

[F2]

The exponential series is absolutely convergent for a bounded matrix operator (The exponential series of a bounded operator).

Verification

1.1givenF1algebra

Write $A = - I + 10 N$ with $N = (\begin{array}{cc} 0 & 1 \\ 0 & 0 \end{array})$ and $N^{2} = 0$ . For $S = diag (10, 1)$ , $A = S (- I + N) S^{- 1}$ . The Jordan formula and similarity invariance in [F1] therefore give $e^{A} = e^{- 1} (I + 10 N) = e^{- 1} (\begin{array}{cc} 1 & 10 \\ 0 & 1 \end{array})$ . Direct multiplication gives $A^{*} A = (\begin{array}{cc} 1 & - 10 \\ - 10 & 101 \end{array})$ and $A A^{*} = (\begin{array}{cc} 101 & - 10 \\ - 10 & 1 \end{array})$ , so $A$ is nonnormal.

2.1F2step 1.1algebra∎

The row-sum norm is $11 / e$ , while the spectral radius of $e^{A}$ is $e^{- 1} < 1$ . From [F2], $e = \sum_{k \geq 0} 1 / k! < 3$ (for $k \geq 1$ , $k! \geq 2^{k - 1}$ , with strict inequality for some terms). Thus $11 / e > 1$ , displaying transient norm growth despite the stable eigenvalues.

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

A half-turn lies on the principal logarithm branch cut

Example

The planar half-turn $R_{π} = - I_{2}$ is invertible, and the principal logarithm algorithm must return a branch-domain failure because its spectrum lies on the removed negative-real axis.

Facts & Assumptions

Given: $R_{π} = - I_{2}$ , the principal logarithm request, and finite complex Francis controls with deflation tolerance $0$ , sweep budget $0$ , stagnation period $1$ , and an empty exceptional-shift table for both Schur calls. The Schur–Parlett threshold is $0$ , its initial partition is the two singletons, and its interval-keyed table contains the exact $1 \times 1$ Jordan certificate $Z = [1]$ , $J = [- 1]$ for each singleton. These block data are not used because the branch test fails first.

[F1]

The holomorphic principal logarithm is defined on $S = C ∖ (- \infty, 0]$ (The principal logarithm is the normalised holomorphic branch on the slit plane).

[F2]

The branch-aware procedure returns branch-domain-failure when an exact Schur diagonal eigenvalue lies in $(- \infty, 0]$ (Principal matrix logarithm and square root by branch-aware Schur–Parlett).

[F3]

With sweep budget $0$ , a complex Francis reduction returns Schur-computed when the initialized matrix is already upper triangular; when $n = 2$ its Hessenberg initialization has no reflector columns (Finite-budget computed Francis Schur reduction with explicit statuses).

Verification

1.1givenF1algebra

The characteristic polynomial of $R_{π}$ is $(z + 1)^{2}$ , so its only eigenvalue is $- 1$ . This lies on the removed ray and hence outside $S$ by [F1].

2.1F2F3step 1.1algebra∎

Here $n = 2$ , so [F3] performs no Hessenberg reflectors. The initialized matrix $- I_{2}$ is already upper triangular, and with zero sweeps the reduction returns the exact pair $Q = I_{2}$ , $T = - I_{2}$ ; this pair passes $Q^{*} Q = I$ and $A = Q T Q^{*}$ . The branch test then sees the diagonal value $- 1$ and returns branch-domain-failure by [F2]. This records only that the principal holomorphic branch is unavailable there.

Matrix Functions and Scaling Squaring — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

A positive diagonal Gram matrix gives a nontrivial polar factor

Example

Facts & Assumptions

Verification

A stable-spectrum nonnormal exponential has a large transient norm

Example

Facts & Assumptions

Verification

A half-turn lies on the principal logarithm branch cut

Example

Facts & Assumptions

Verification

Sources