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.

CSR storage and exact matrix-vector operation counts

Statement

Let $F$ be a field, let $m, n \in N$ , and let a valid CSR record have $s$ stored entries. Its input arrays use exactly $s$ field-value slots, $s$ integer column-index slots, and $m + 1$ integer row-pointer slots, for a total of $2 s + m + 1$ data slots. On valid input, the algorithm Validated compressed sparse row matrix-vector product performs exactly $s$ field multiplications, $s$ field additions, and $m$ zero initializations. Its index validation and loop-control work is $O (m + s + 1)$ . Counting the CSR arrays and returned output but excluding the supplied vector $x$ and constant-size workspace, it uses exactly $2 s + 2 m + 1$ data slots, hence $O (m + s + 1)$ slots; for $m \geq 1$ this is $O (m + s)$ . Here $O (g)$ means bounded by $C g$ for a constant $C$ independent of the dimensions and input values.

For a square record of order $m \geq 1$ with at least one stored entry in each row, $s \geq m$ , so the work and storage are $O (s)$ . For a canonical record as defined in Compressed sparse row matrices with stored-entry semantics, $s = nnz (A)$ ; without that convention, the cost is in terms of stored entries, not $nnz (A)$ . These are arithmetic, index, and storage counts, not runtime, memory-bandwidth, convergence, or factorization-cost bounds.

Facts & Assumptions

Given: A valid CSR record with dimensions $m, n \in N$ and $s$ stored entries.

[L1]

Compressed sparse row matrices with stored-entry semantics: the arrays have lengths $m + 1$ , $s$ , and $s$ ; the row pointers satisfy $r_{0} = 0 \leq \dots \leq r_{m} = s$ .

[L2]

Compressed sparse row matrices with stored-entry semantics: a record is canonical when no row repeats a column and no stored value is zero; then $s = nnz (A)$ .

[L3]

Validated compressed sparse row matrix-vector product: on a valid record the algorithm initializes $m$ outputs and visits each row interval $r_{i}, \dots, r_{i + 1} - 1$ , performing one multiply-add per visited index.

Proof

1.1L1algebra

The value, column-index, and row-pointer arrays have lengths $s$ , $s$ , and $m + 1$ , respectively, so their input representation contains exactly $2 s + m + 1$ data slots.

1.2L1L3algebra

The number of visits in row $i$ is $r_{i + 1} - r_{i}$ . Summing these lengths telescopes to $r_{m} - r_{0} = s$ ; monotonicity makes the intervals disjoint and their endpoints cover every stored index once. Thus the accumulation loop executes exactly $s$ multiply-add updates, and the initialization loop executes exactly $m$ times. The two validation scans examine at most $m + 1$ pointers and $s$ column indices, so validation and loop control take $O (m + s + 1)$ work.

1.3L1L3algebra

The returned vector occupies $m$ additional field slots. Counting it with the CSR arrays, and excluding the supplied $x$ and fixed workspace, gives exactly $2 s + 2 m + 1$ data slots, hence $O (m + s + 1)$ . If $m \geq 1$ , then $m + s \geq 1$ and the additive constant is absorbed into a fixed multiple of $m + s$ .

2.1L1L2step 1.2step 1.3algebra∎

For a square record of order $m \geq 1$ with every row storing at least one entry, summing its $m$ row lengths gives $s \geq m$ ; substituting into the preceding bounds yields $O (s)$ . By [L2], a canonical record has $s = nnz (A)$ ; no such equality is asserted when duplicate columns or explicit zeros are stored.

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.4–3.5, printed pp. 92–96 (standard reference, not scraped)
Richard Barrett et al., Templates for the Solution of Linear Systems: Building Blocks for Iterative Methods, 2nd ed., Chapter 4 §4.3.1–4.3.2, printed pp. 57–63 (standard reference, not scraped)