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

Error propagation through exact and perturbed squaring steps

Statement

Let $∥ \cdot ∥$ be a submultiplicative norm on square matrices. Suppose $X_{j + 1} = X_{j}^{2}$ and ${\hat{X}}_{j + 1} = {\hat{X}}_{j}^{2} + E_{j}$ for matrices of the same size. If $e_{j} = ∥ {\hat{X}}_{j} - X_{j} ∥$ , then $e_{j + 1} \leq (2 ∥ X_{j} ∥ + e_{j}) e_{j} + ∥ E_{j} ∥ .$ The term $E_{j}$ records the entire defect in the computed squaring.

Facts & Assumptions

Given: The matrices and recurrence above, and a matrix norm satisfying $∥ U V ∥ \leq ∥ U ∥ ∥ V ∥$ for every compatible product.

[A1]

The chosen matrix norm is submultiplicative, as stated in the hypotheses.

Proof

1.1givenalgebra

Put $D_{j} = {\hat{X}}_{j} - X_{j}$ . The noncommutative identity ${\hat{X}}_{j}^{2} - X_{j}^{2} = D_{j} {\hat{X}}_{j} + X_{j} D_{j}$ follows by expanding the right side and cancelling $- X_{j} {\hat{X}}_{j} + X_{j} {\hat{X}}_{j}$ .

2.1A1step 1.1algebra

By [A1] and the triangle inequality, $∥ {\hat{X}}_{j}^{2} - X_{j}^{2} ∥ \leq e_{j} ∥ {\hat{X}}_{j} ∥ + ∥ X_{j} ∥ e_{j}$ ; also $∥ {\hat{X}}_{j} ∥ \leq ∥ X_{j} ∥ + e_{j}$ . Hence $∥ {\hat{X}}_{j}^{2} - X_{j}^{2} ∥ \leq (2 ∥ X_{j} ∥ + e_{j}) e_{j}$ .

3.1givenstep 2.1algebra∎

The identity ${\hat{X}}_{j + 1} - X_{j + 1} = ({\hat{X}}_{j}^{2} - X_{j}^{2}) + E_{j}$ and step 2.1 give the claimed bound by the triangle inequality.

Used by

Dependency tree · 0 levels

Nothing. This result depends on no other item in the library.

Sources

Jan Zur, Matrix Functions, TU Berlin full lecture notes (standard reference, not scraped)
Awad H. Al-Mohy and Nicholas J. Higham, A New Scaling and Squaring Algorithm for the Matrix Exponential (standard reference, not scraped)