TheoremStatement: AI-adaptedProof: AI-generatedPipeline-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.

The filled graph contains every off-diagonal Schur-complement nonzero

Statement

Let $F$ be a field, let $A \in M_{n \times n} (F)$ satisfy $A_{i j} = A_{j i}$ for all $i, j < n$ , and fix an elimination ordering. Let $G_{k} = (V_{k}, E_{k})$ be its symbolic filled graphs from Structural graphs and ordered symmetric elimination. Put $S^{0} = A$ . Assume each pivot $p_{k} : = S_{v_{k} v_{k}}^{k}$ is nonzero, and for every pair of remaining vertices define the Schur update

$S_{i j}^{k + 1} : = S_{i j}^{k} - \frac{S_{i v_{k}}^{k} S_{v_{k} j}^{k}}{p_{k}} .$

Then for every stage $k$ , each nonzero off-diagonal entry $S_{i j}^{k}$ has ${i, j} \in E_{k}$ . At each elimination step, the later neighbors of the eliminated vertex form a clique in the next filled graph. Thus the symbolic filled graph contains each numerical Schur complement's off-diagonal support; equality of these off-diagonal patterns is not asserted.

Facts & Assumptions

Given: A field $F$ , a symmetric matrix in $M_{n \times n} (F)$ , a fixed elimination ordering, nonzero pivots, and the Schur-complement update in the Statement.

[L1]

Structural graphs and ordered symmetric elimination: at step $k$ , the graph deletes $v_{k}$ , retains edges between remaining vertices, and adds every edge between distinct vertices of $N_{k} (v_{k})$ .

[L2]

Field: division by a nonzero pivot means multiplication by its multiplicative inverse.

[L3]

Multiplication by zero: $0 \cdot a = 0$ : in a field, $0 \cdot a = 0$ for every $a$ .

[L4]

A field has no zero divisors: $a b = 0 \Rightarrow a = 0$ or $b = 0$ : in a field, $a b = 0$ implies $a = 0$ or $b = 0$ .

[A1]

For every $k < n$ , $p_{k} \neq 0$ and $S_{i j}^{k + 1} = S_{i j}^{k} - S_{i v_{k}}^{k} S_{v_{k} j}^{k} / p_{k}$ for all $i, j \in V_{k + 1}$ .

Proof

1.1givenL1algebra

At stage $0$ , $S^{0} = A$ and the initial edge set consists exactly of the unordered off-diagonal pairs with nonzero matrix entry. Hence every nonzero off-diagonal entry of $S^{0}$ corresponds to an edge of $G_{0}$ .

1.2A1L1L2L3L4inductionalgebra

Suppose the support inclusion holds at stage $k$ . If $S_{i j}^{k + 1} \neq 0$ for distinct $i, j \in V_{k + 1}$ , then at least one of $S_{i j}^{k}$ and $S_{i v_{k}}^{k} S_{v_{k} j}^{k} / p_{k}$ is nonzero. In the first case, the induction hypothesis gives ${i, j} \in E_{k}$ , and the update retains that edge. In the second case, the numerator is nonzero because a zero numerator would give a zero quotient by [L2] and [L3]; then [L4] forces both pivot couplings to be nonzero. The induction hypothesis gives ${i, v_{k}}, {v_{k}, j} \in E_{k}$ , so $i, j \in N_{k} (v_{k})$ and the update adds ${i, j}$ . Thus every such nonzero is supported by an edge of $G_{k + 1}$ .

2.1step 1.1step 1.2L1induction∎

The base case and induction step prove the support inclusion at every stage. For any two distinct later neighbors of $v_{k}$ , the graph update inserts their pair by definition, so the later-neighbor set is a clique in $G_{k + 1}$ .

Remarks

The conclusion is a support inclusion, not equality: an arithmetic subtraction can cancel a nonzero entry while the symbolic edge remains. The companion page gives an explicit cancellation calculation in Numerical cancellation can zero an entry while the filled graph retains its edge ↗. No factorization-cost bound follows from this graph statement.

Depends on

Used by

Dependency tree · two levels

5 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

Yousef Saad, Iterative Methods for Sparse Linear Systems, 2nd ed., Chapter 3 §§3.2.1, 3.3.2 and 3.6, printed pp. 77–83 and 96–98 (standard reference, not scraped)
Prabhakar Poupart and Jingjing Wan, CS475/CS675 Lecture 4: Sparse Gaussian Elimination, Graph Representation, slides 6–10, University of Waterloo, May 12, 2016 (standard reference, not scraped)