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

One exact scalar elimination step updates a displacement generator

Statement

Let $n \geq 2$ , let $A = (\begin{array}{cc} d & r^{*} \\ ℓ & M \end{array}) \in C^{n \times n}$ with $d \neq 0$ , and let $s \geq 1$ be an integer. Let $Z_{n} = (\begin{array}{cc} 0 & 0 \\ e_{0} & Z_{n - 1} \end{array})$ be the lower shift partitioned after its first row and column. Suppose $A - Z_{n} A Z_{n}^{*} = G H^{*}, G = (\begin{array}{c} \hat{G} \\ G_{b} \end{array}), H = (\begin{array}{c} \hat{H} \\ H_{b} \end{array}),$ where $G, H \in C^{n \times s}$ , $\hat{G}, \hat{H} \in C^{1 \times s}$ , and $G_{b}, H_{b} \in C^{(n - 1) \times s}$ . Let $S : = M - ℓ d^{- 1} r^{*}$ be the scalar-pivot Schur complement. Define $p : = e_{0} + (Z_{n - 1} ℓ - ℓ) / d, q : = e_{0} + (Z_{n - 1} r - r) / \overline{d}, G^{'} : = G_{b} + p \hat{G}, H^{'} : = H_{b} + q \hat{H} .$ Then $S - Z_{n - 1} S Z_{n - 1}^{*} = G^{'} H^{' *} .$ Thus the updated displacement rank is at most $s$ , although it can decrease. This is an exact identity conditional on the nonzero pivot $d$ ; it makes no conditioning or growth claim.

Facts & Assumptions

Given: The block matrix $A$ , nonzero scalar pivot $d$ , lower shifts, and a width- $s$ generator $G, H$ for $A - Z_{n} A Z_{n}^{*}$ .

[F1]

The lower shift and displacement are $Z_{n}$ and $A - Z_{n} A Z_{n}^{*}$ . Lower-shift displacement rank and generator pairs

[F2]

Eliminating an invertible leading block uses the Schur complement $A_{22} - A_{21} A_{11}^{- 1} A_{12}$ . Block LU factorisation and the associated Schur complement

[F3]

Matrix products are evaluated by their finite entry sums. Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes Here $B^{*}$ denotes the conjugate transpose, $(B^{*})_{i j} : = \overline{B_{j i}}$ .

Proof

1.1F1F3algebra

Write $e = e_{0} \in C^{n - 1}$ and $Z^{'} = Z_{n - 1}$ . Direct block multiplication using [F3] gives $Z_{n} A Z_{n}^{*} = (\begin{array}{cc} 0 & 0 \\ 0 & (e d + Z^{'} ℓ) e^{*} + (e r^{*} + Z^{'} M) Z^{' *} \end{array}) .$ Therefore the first row and column of $A - Z_{n} A Z_{n}^{*}$ are $(d, r^{*})$ and $(d, ℓ)^{T}$ , while its lower-right block is $M - Z^{'} M Z^{' *} - d e e^{*} - Z^{'} ℓ e^{*} - e r^{*} Z^{' *} .$

2.1givenstep 1.1algebra

Comparing the four blocks of $G H^{*} = A - Z_{n} A Z_{n}^{*}$ in step 1.1 gives $\hat{G} {\hat{H}}^{*} = d$ , $G_{b} {\hat{H}}^{*} = ℓ$ , $\hat{G} H_{b}^{*} = r^{*}$ , and $G_{b} H_{b}^{*} = M - Z^{'} M Z^{' *} - d e e^{*} - Z^{'} ℓ e^{*} - e r^{*} Z^{' *} .$

3.1F2step 2.1algebra

From the definitions of $G^{'}$ and $H^{'}$ , $G^{'} H^{' *} = G_{b} H_{b}^{*} + ℓ q^{*} + p r^{*} + d p q^{*} .$ Here $q^{*} = e^{*} + (r^{*} Z^{' *} - r^{*}) / d$ and $p = e + (Z^{'} ℓ - ℓ) / d$ . Expand them separately: $ℓ q^{*} = ℓ e^{*} + (ℓ r^{*} Z^{' *} - ℓ r^{*}) / d, p r^{*} = e r^{*} + (Z^{'} ℓ r^{*} - ℓ r^{*}) / d,$ $d p q^{*} = d e e^{*} + e r^{*} Z^{' *} - e r^{*} + (Z^{'} ℓ - ℓ) e^{*} + ((Z^{'} ℓ - ℓ) (r^{*} Z^{' *} - r^{*})) / d .$ The non-fractional terms combine to $d e e^{*} + Z^{'} ℓ e^{*} + e r^{*} Z^{' *}$ , and the common fractional numerator simplifies by distributivity: $ℓ r^{*} Z^{' *} - ℓ r^{*} + Z^{'} ℓ r^{*} - ℓ r^{*} + (Z^{'} ℓ - ℓ) r^{*} Z^{' *} - (Z^{'} ℓ - ℓ) r^{*} = - ℓ r^{*} + Z^{'} ℓ r^{*} Z^{' *} .$ Thus $ℓ q^{*} + p r^{*} + d p q^{*} = d e e^{*} + Z^{'} ℓ e^{*} + e r^{*} Z^{' *} - ℓ r^{*} / d + Z^{'} ℓ r^{*} Z^{' *} / d,$ as required. Substituting [F2] and step 2.1 now yields $G^{'} H^{' *} = M - Z^{'} M Z^{' *} - ℓ r^{*} / d + Z^{'} ℓ r^{*} Z^{' *} / d = S - Z^{'} S Z^{' *} .$

4.1step 3.1algebra∎

The factors $G^{'}, H^{'}$ each have $s$ columns, so their product has rank at most $s$ . A strict rank decrease is possible when columns become dependent; no exact rank preservation or numerical growth bound is asserted.

Remarks

The source's general generator block-update lemma states the same structural fact for a block pivot. The scalar lower-shift specialization above supplies its full algebraic verification. A nonzero pivot permits this exact update; it does not guarantee a well-conditioned or small-growth elimination.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

8 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

Daniel Kressner and Robert Luce, Fast computation of the matrix exponential for a Toeplitz matrix, Lemma 3.1 (standard reference, not scraped)