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

Filled edges are witnessed by paths through earlier eliminated vertices

Statement

Use the zero-based graph and ordering of Structural graphs and ordered symmetric elimination. For distinct remaining vertices $x, y \in V_{k}$ , the pair ${x, y}$ is an edge of $G_{k}$ if and only if the original graph $G_{0}$ contains a finite walk from $x$ to $y$ all of whose internal vertices belong to ${v_{0}, \dots, v_{k - 1}}$ . A walk may repeat vertices; its internal vertices are the entries other than its two endpoints.

Facts & Assumptions

Given: A finite simple graph, an elimination ordering, and the filled graphs defined by the supplier.

[F1]

Structural graphs and ordered symmetric elimination: At step $k$ , delete $v_{k}$ , retain edges between remaining vertices, and add every pair of distinct later neighbors of $v_{k}$ .

Proof

1.1givenF1basealgebra

At $k = 0$ , a walk with no internal vertices consists of one edge, so the claimed equivalence is exactly the definition of $G_{0}$ .

1.2F1IHinductionalgebra

Suppose the equivalence holds at stage $k$ . A retained edge in $G_{k + 1}$ already has a witnessing walk whose internal vertices are among $v_{0}, \dots, v_{k - 1}$ . An edge newly added at step $k$ joins two vertices $x, y$ that are each adjacent to $v_{k}$ in $G_{k}$ . The induction hypothesis gives walks from $x$ to $v_{k}$ and from $v_{k}$ to $y$ with internal vertices among $v_{0}, \dots, v_{k - 1}$ ; concatenating them gives the required walk with the additional internal vertex $v_{k}$ . This proves the forward implication at stage $k + 1$ .

2.1F1IHstep 1.2inductionalgebra

Conversely, let a witnessing walk from $x$ to $y$ have internal vertices among $v_{0}, \dots, v_{k}$ . If it has no internal occurrence of $v_{k}$ , the induction hypothesis gives an edge in $G_{k}$ , which is retained. Otherwise take the first and last internal occurrences of $v_{k}$ . The initial subwalk from $x$ to the first occurrence and the terminal subwalk from the last occurrence to $y$ have all internal vertices among $v_{0}, \dots, v_{k - 1}$ . By induction, $x$ and $y$ are both later neighbors of $v_{k}$ in $G_{k}$ . Since $x \neq y$ , the update inserts ${x, y}$ in $G_{k + 1}$ .

3.1step 1.1step 1.2step 2.1discharge-induction∎

The base case and steps 1.2 and 2.1 prove both implications for every stage by induction on $k$ .

Depends on

Structural graphs and ordered symmetric elimination

Used by

Dependency tree · two levels

3 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 4, §§4.1–4.3 (standard reference, not scraped)
Timothy A. Davis, Siva Rajamanickam, and Wissam M. Sid-Lakhdar, A survey of direct methods for sparse linear systems, §4 (standard reference, not scraped)