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.

Every later filled neighbor lies on the elimination-tree parent path

Statement

Let $v_{k}$ be a vertex in the elimination forest supplied by Elimination-tree column patterns and reach. Every later filled neighbor of $v_{k}$ lies on its parent path and is therefore an ancestor. Consequently, if $v_{s}$ is a child of $v_{k}$ , then every later neighbor of $v_{s}$ other than $v_{k}$ is a later neighbor of $v_{k}$ ; equivalently, $C_{s} ∖ {v_{s}} \subseteq C_{k} .$

Facts & Assumptions

Given: The zero-based ordered vertices, filled graphs, and parent forest from batch-2's graph definition.

[F1]

Elimination-tree column patterns and reach: $C_{k} = {v_{k}} \cup N_{k} (v_{k})$ , and reach follows the supplied parent path.

[F2]

Structural graphs and ordered symmetric elimination: The parent is the later neighbor with least position greater than the child's position.

[F3]

Structural graphs and ordered symmetric elimination: The graph update adds every edge between two distinct vertices in the pivot's later-neighbor set.

Proof

1.1givenF2F3choose

Fix $v_{k}$ and a later filled neighbor $v_{t}$ . If $v_{t}$ is the parent, it is an ancestor by definition. Otherwise let $v_{s}$ be the parent. By [F2], $k < s < t$ . Since $v_{s}$ and $v_{t}$ are both later neighbors of $v_{k}$ , [F3] inserts ${v_{s}, v_{t}}$ when $v_{k}$ is eliminated. Thus $v_{t}$ remains a later neighbor of $v_{s}$ .

1.2F1F2F3algebra

Now let $v_{s}$ be a child of $v_{k}$ . Every later neighbor $v_{t}$ of $v_{s}$ is either $v_{k}$ or is later than $v_{k}$ . In the latter case both $v_{k}$ and $v_{t}$ are later neighbors of $v_{s}$ , so [F3] joins them in the filled graph. Thus every element of $C_{s} ∖ {v_{s}}$ belongs to $C_{k}$ .

2.1step 1.1F2inductionalgebra

If $v_{t}$ is not the parent of $v_{s}$ , replace $v_{k}$ by $v_{s}$ and repeat. At each repetition the ordering position strictly increases and is at most $t$ , because the current vertex remains adjacent to $v_{t}$ and its parent is the earliest later neighbor. The finite increasing sequence must reach position $t$ ; it cannot stop earlier at a root while still having later neighbor $v_{t}$ . Hence $v_{t}$ lies on the parent path from $v_{k}$ and is an ancestor.

3.1step 2.1step 1.2∎

Step 2.1 proves the ancestor assertion, and step 1.2 gives the child-column containment used to assemble fronts.

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

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