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 matrix-vector multiplication returns the represented product

Statement

Let $F$ be a field, let $m, n \in N$ , let a valid CSR record represent $A \in M_{m \times n} (F)$ , and let $x = (x_{j})_{j < n} \in F^{n}$ . Let $X \in M_{n \times 1} (F)$ be the column matrix with $X_{j 0} = x_{j}$ for $j < n$ , and define $A x \in F^{m}$ by $(A x)_{i} : = (A X)_{i 0} = \sum_{j < n} A_{i j} x_{j} (i < m),$ using Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes. Then the algorithm Validated compressed sparse row matrix-vector product returns ok with output $A x$ in exact field arithmetic.

Facts & Assumptions

Given: A field $F$ , $m, n \in N$ , a valid CSR record representing $A$ , and $x \in F^{n}$ .

[L1]

Compressed sparse row matrices with stored-entry semantics: $A_{i j} = \sum_{r_{i} \leq t < r_{i + 1}} 1_{c_{t} = j} v_{t}$ , with an empty sum equal to $0_{F}$ .

[L2]

Validated compressed sparse row matrix-vector product: each row starts at $0_{F}$ and accumulates $v_{t} x_{c_{t}}$ once for every $t = r_{i}, \dots, r_{i + 1} - 1$ .

[L3]

Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes: for the column matrix $X$ with $X_{j 0} = x_{j}$ , $(A X)_{i 0} = \sum_{j < n} A_{i j} x_{j}$ .

[L4]

A finite sum in a commutative monoid indexed by an arbitrary finite set: a finite sum is independent of its enumeration and an empty sum is its identity element.

[L5]

Field: multiplication distributes over addition.

[L6]

The vector space $F^{X}$ of all functions $X \to F$ with pointwise operations, and $F^{n}$ as the case $X = n = {0, 1, \dots, n - 1}$ : $F^{m}$ is the set of functions $m \to F$ ; when $m = 0$ it has exactly one element, the empty function.

[L7]

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

[L8]

Field: multiplication is commutative on all of $F$ , and $x \cdot 1 = x$ for every $x \in F$ ; hence $1_{F} x = x$ .

Proof

1.1L2inductionalgebra

Fix a row $i$ . Initially its output coordinate is $0_{F}$ , the empty partial sum. After $q$ entries of that row have been visited, induction on $q$ gives $y_{i} = \sum_{t = r_{i}}^{r_{i} + q - 1} v_{t} x_{c_{t}}$ : the next algorithmic update adds exactly the next summand. Taking $q = r_{i + 1} - r_{i}$ yields $y_{i} = \sum_{r_{i} \leq t < r_{i + 1}} v_{t} x_{c_{t}}$ .

2.1L1L3L4L5L7L8step 1.1algebra

By [L1] and [L3], $(A x)_{i} = \sum_{j < n} \sum_{r_{i} \leq t < r_{i + 1}} 1_{c_{t} = j} v_{t} x_{j}$ . Repeated application of [L5], by induction on the finite number of summands, distributes the products over these sums. Re-enumerating the resulting finite sum over pairs $(j, t)$ as $(t, j)$ is permitted by [L4]. For each fixed $t$ , exactly the term $j = c_{t}$ survives, so the result is $\sum_{r_{i} \leq t < r_{i + 1}} v_{t} x_{c_{t}}$ . By step 1.1 this equals $y_{i}$ .

3.1L6step 2.1algebra∎

If $m = 0$ , both $y$ and $A x$ are the unique empty vector by [L6]. If $m > 0$ , step 2.1 gives equality in every coordinate $i < m$ , hence $y = A x$ .

Depends on

Used by

Dependency tree · two levels

18 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)