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

Block LDL* residual errors propagate with actual block growth

Statement

Consider a successful run of Sparse symmetric-indefinite block LDL* with threshold tests and failure status on a Hermitian input with its declared permutation $P$ and fixed pivot-block sequence. In every formula, $∥ X ∥_{2}$ is the operator norm induced by the Euclidean inner products. At stage $r$ , write the active matrix as $(\begin{array}{cc} D_{r} & B_{r}^{*} \\ B_{r} & C_{r} \end{array}) .$ Suppose the computed trailing block is ${\hat{S}}_{r + 1} = C_{r} - B_{r} D_{r}^{- 1} B_{r}^{*} + Δ_{r},$ where $Δ_{r}$ is the exact local update residual. Embed it into the full permuted coordinates as $E_{r}$ , with zeros on all previously eliminated and current pivot indices. Let $T_{r}$ be the $n \times n$ identity on previously eliminated coordinates and the padded unit lower block elimination matrix $(\begin{array}{cc} I & 0 \\ B_{r} D_{r}^{- 1} & I \end{array})$ on the current pivot and trailing coordinates. Set $W_{1} = I$ and $W_{r} = T_{1} \dots T_{r - 1}$ for $r > 1$ . Then $∥ P A P^{*} - L_{e x} D_{b l k} L_{e x}^{*} ∥_{2} \leq \sum_{r} ∥ W_{r} ∥_{2}^{2} ∥ Δ_{r} ∥_{2} \leq ρ_{b l k} \sum_{r} η_{r} (∥ C_{r} ∥_{2} + ∥ B_{r} ∥_{2}^{2} ∥ D_{r}^{- 1} ∥_{2}),$ provided the actual local residuals satisfy $∥ Δ_{r} ∥_{2} \leq η_{r} (∥ C_{r} ∥_{2} + ∥ B_{r} ∥_{2}^{2} ∥ D_{r}^{- 1} ∥_{2}) .$ Here $L_{e x}$ is the product of the exact-multiplier transformations $T_{r}$ , not a rounded stored multiplier factor. For a nonempty run, $ρ_{b l k} : = \max_{r} ∥ W_{r} ∥_{2}^{2}$ is the actual amplification from this pivot sequence. For an empty pivot partition set $ρ_{b l k} = 0$ ; all stage sums are then zero. The trailing-only statement is conditional in this general form. For the specified kernel, Hermitian block LDL* kernels have explicit roundoff and actual-factor residual bounds proves it with $η_{r} = η_{k_{r}, t_{r}}$ , retaining the actual normalized-determinant and range certificates. It makes no uniform smallness claim for $ρ_{b l k}$ , $∥ D_{r}^{- 1} ∥_{2}$ , or $η_{r}$ .

In exact arithmetic every accepted block is nonsingular and each update has $Δ_{r} = 0$ , so a successful run returns $P A P^{*} = L D_{b l k} L^{*}$ .

For the actual rounded output, let ${\hat{T}}_{r}$ be the $n \times n$ transformation built from stored ${\hat{M}}_{r}$ , padded by the identity on previously eliminated coordinates. Let $F_{r, a c t}$ be the $(k_{r} + t_{r}) \times (k_{r} + t_{r})$ reconstruction residual from the local kernel lemma, and define $F_{r}$ by embedding $F_{r, a c t}$ into the current pivot and trailing coordinates, with zero rows and columns on all previously eliminated indices. Set ${\hat{W}}_{1} = I_{n}$ and ${\hat{W}}_{r} = {\hat{T}}_{1} \dots {\hat{T}}_{r - 1}$ . Then $P A P^{*} - \hat{L} D_{b l k} {\hat{L}}^{*} = \sum_{r} {\hat{W}}_{r} F_{r} {\hat{W}}_{r}^{*}, ∥ P A P^{*} - \hat{L} D_{b l k} {\hat{L}}^{*} ∥_{2} \leq \sum_{r} ∥ {\hat{W}}_{r} ∥_{2}^{2} f_{r} \leq {\hat{ρ}}_{b l k} \sum_{r} f_{r},$ where $f_{r}$ is the proved explicit local bound. For a nonempty run set ${\hat{ρ}}_{b l k} = \max_{r} ∥ {\hat{W}}_{r} ∥_{2}^{2}$ , and for an empty pivot partition set ${\hat{ρ}}_{b l k} = 0$ . This includes multiplier coupling residuals as well as trailing updates. Neither actual growth nor inverse-pivot conditioning is assumed uniformly small.

Facts & Assumptions

Given: A successful sequence of Hermitian $1 \times 1$ or $2 \times 2$ pivots, the actual local update residuals $Δ_{r}$ , and the displayed local error bounds.

[F1]

Sparse symmetric-indefinite block LDL* with threshold tests and failure status: The declared permutation is applied once; each accepted pivot block is Hermitian and nonsingular, and the exact trailing update is $C - B D^{- 1} B^{*}$ .

[F2]

The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||: For a linear map between finite-dimensional inner-product spaces, the operator norm is the maximum of $∥ T v ∥$ over unit vectors (and is zero on the zero domain).

[A1]

For each stage $r$ , the computed trailing block is $C_{r} - B_{r} D_{r}^{- 1} B_{r}^{*} + Δ_{r}$ and $∥ Δ_{r} ∥_{2} \leq η_{r} (∥ C_{r} ∥_{2} + ∥ B_{r} ∥_{2}^{2} ∥ D_{r}^{- 1} ∥_{2})$ .

[F3]

Hermitian block LDL* kernels have explicit roundoff and actual-factor residual bounds proves the concrete local trailing residual, exact pivot acceptance, and full stored-multiplier reconstruction residual.

Proof

1.1givenF1algebra

For each accepted block, $D_{r}$ is invertible by its pivot test. Direct block multiplication gives $(\begin{array}{cc} D_{r} & B_{r}^{*} \\ B_{r} & C_{r} \end{array}) = (\begin{array}{cc} I & 0 \\ B_{r} D_{r}^{- 1} & I \end{array}) (\begin{array}{cc} D_{r} & 0 \\ 0 & C_{r} - B_{r} D_{r}^{- 1} B_{r}^{*} \end{array}) (\begin{array}{cc} I & D_{r}^{- 1} B_{r}^{*} \\ 0 & I \end{array}),$ with the right-hand side an ordinary matrix product. Thus in exact arithmetic each elimination step is a valid Hermitian congruence. In the increasing-stage product $T_{1} \dots T_{r}$ , the earlier factors act as the identity on columns supported on the still-active coordinates, so multiplication by $T_{r}$ inserts precisely the stored multiplier columns for $J_{r}$ . The product is therefore the stored unit lower block-triangular $L$ , and completion gives $P A P^{*} = L D_{b l k} L^{*}$ with block-diagonal $D_{b l k}$ ; empty products give the empty identity.

1.2givenF1basealgebra

With a computed update, the middle trailing block differs by $Δ_{r}$ . Hence the reconstructed active matrix at stage $r$ differs from the block factorization with ${\hat{S}}_{r + 1}$ by the embedded matrix whose only nonzero block is $- Δ_{r}$ in the trailing coordinates.

2.1step 1.2F1IHinductionalgebra

Substitute the next-stage factorization into the trailing block of step 1.2. The local residual from stage $r + 1$ is conjugated by the padded stage- $r$ lower elimination transformation. Repeated substitution therefore yields $P A P^{*} - L_{e x} D_{b l k} L_{e x}^{*} = - \sum_{r} W_{r} E_{r} W_{r}^{*} .$ After one stage this is step 1.2. Replacing the next trailing block adds $- T_{1} E_{2} T_{1}^{*}$ ; each later substitution adds the next embedded residual conjugated by all preceding $T_{h}$ . Induction on the number of processed pivot blocks gives exactly $W_{r} = T_{1} \dots T_{r - 1}$ and the displayed identity.

3.1F2step 2.1algebra

For any compatible maps $X, Y$ , [F2] gives $∥ X Y v ∥_{2} \leq ∥ X ∥_{2} ∥ Y v ∥_{2} \leq ∥ X ∥_{2} ∥ Y ∥_{2} ∥ v ∥_{2}$ , so $∥ X Y ∥_{2} \leq ∥ X ∥_{2} ∥ Y ∥_{2}$ . If $E_{r}$ is the zero-padded trailing block $Δ_{r}$ , then $∥ E_{r} x ∥_{2} = ∥ Δ_{r} x_{t a i l} ∥_{2} \leq ∥ Δ_{r} ∥_{2} ∥ x_{t a i l} ∥_{2} \leq ∥ Δ_{r} ∥_{2} ∥ x ∥_{2}$ , hence $∥ E_{r} ∥_{2} \leq ∥ Δ_{r} ∥_{2}$ . Also $∥ X^{*} ∥_{2} = ∥ X ∥_{2}$ : express the Euclidean norm as $\sup_{∥ v ∥ = 1} ∣ ⟨ v, w ⟩ ∣$ by Cauchy-Schwarz and take the two finite unit-vector suprema in either order. These inequalities and the triangle inequality bound each summand in step 2.1 by $∥ W_{r} ∥_{2}^{2} ∥ Δ_{r} ∥_{2}$ and give the first asserted bound.

4.1step 3.1A1discharge-inductionalgebra

Apply [A1] to each $Δ_{r}$ in step 3.1 and use $∥ W_{r} ∥_{2}^{2} \leq ρ_{b l k}$ . Summing gives the second bound. Since every $D_{r}$ is invertible but may be ill-conditioned and the transformation products may grow, no universal stability constant follows.

5.1F3step 3.1step 4.1algebra

For each accepted concrete kernel apply [F3]. Its $η_{k_{r}, t_{r}}$ supplies [A1], so steps 1.1, 1.2, 2.1, 3.1, and 4.1 give the claimed trailing-only estimate for the conceptual $L_{e x}$ . For actual stored multipliers, let ${\hat{T}}_{r, a c t}$ be the active block of ${\hat{T}}_{r}$ . Then [F3] gives the active identity $A_{r} = {\hat{T}}_{r, a c t} diag (D_{r}, {\hat{S}}_{r + 1}) {\hat{T}}_{r, a c t}^{*} + F_{r, a c t}$ , including the off-diagonal residual $N_{r} = {\hat{M}}_{r} D_{r} - B_{r}$ . Padding this identity uses $F_{r}$ as defined above; zero-padding preserves its operator norm, so $∥ F_{r} ∥_{2} = ∥ F_{r, a c t} ∥_{2} \leq f_{r}$ .

6.1F1F2F3step 3.1step 5.1inductiondischarge-inductionalgebra∎

Substitute the next active identity into the previous trailing block. After one stage the reconstruction residual is $F_{1}$ ; each additional stage adds its padded $F_{r}$ conjugated by all preceding stored-multiplier transformations. Induction gives $P A P^{*} - \hat{L} D_{b l k} {\hat{L}}^{*} = \sum_{r} {\hat{W}}_{r} F_{r} {\hat{W}}_{r}^{*}$ . The same submultiplicativity from step 3.1 and [F3] give the actual-growth bound. In exact arithmetic every local multiplier and Schur residual is zero, recovering the original exact factorization.

Depends on

Used by

Nothing in the library uses this result yet.

Cited to discharge well-definedness by Sparse symmetric-indefinite block LDL* with threshold tests and failure status.

Dependency tree · two levels

9 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

Jennifer Scott and Miroslav Tůma, Algorithms for Sparse Linear Systems, Chapter 7, §§7.2.4 and 7.3 (standard reference, not scraped)
Timothy A. Davis, Siva Rajamanickam, and Wissam M. Sid-Lakhdar, A survey of direct methods for sparse linear systems, §11 (standard reference, not scraped)