PropositionStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Sparse reduced-cost pricing operation count

Statement

Let $A \in R^{m \times n}$ be represented by a valid CSR record with row pointers $r$ , column indices $c_{t}$ , values $v_{t}$ , and $s$ stored entries, under Compressed sparse row matrices with stored-entry semantics. Matrix and vector coordinates here are zero-based: row $i$ and column $j$ correspond to row $i + 1$ and column $j + 1$ in Basis dictionaries and reduced costs for revised simplex, with the same relabelling for $y, c, w$ and basis-column indices. For each $0 \leq t < s$ , let $i (t)$ be the unique row satisfying $r_{i (t)} \leq t < r_{i (t) + 1}$ . For a cost vector $c \in R^{n}$ and given $y \in R^{m}$ , initialize $w \in R^{n}$ to zero and, for $t = 0, \dots, s - 1$ , update $w_{c_{t}} \leftarrow w_{c_{t}} + v_{t} y_{i (t)} .$ In exact real arithmetic the resulting vector is $A^{T} y$ . This loop uses exactly $s$ multiplications and $s$ additions, preceded by $n$ zero initializations; forming $c - w$ uses $n$ subtractions and gives the reduced-cost vector of Basis dictionaries and reduced costs for revised simplex under the stated relabelling when $y = y (B)$ . Every stored entry is counted, including repeated column indices and explicitly stored zeros. The claim is an arithmetic-operation count; it gives no runtime, bandwidth, or factorization bound.

Facts & Assumptions

Given: A valid CSR record, $y \in R^{m}$ , and exact real arithmetic for the stated updates.

[F1]

Basis dictionaries and reduced costs for revised simplex: For every one-based column index $ℓ$ , its reduced cost is ${\overset{ˉ}{c}}_{ℓ} = c_{ℓ} - a_{ℓ}^{T} y (B)$ ; this item's zero-based column $j$ corresponds to $ℓ = j + 1$ .

[F2]

Compressed sparse row matrices with stored-entry semantics: The stored entries in row $i$ have indices $r_{i} \leq t < r_{i + 1}$ , and the represented coordinate is $A_{i j} = \sum_{r_{i} \leq t < r_{i + 1}} 1_{c_{t} = j} v_{t}$ .

[A1]

The loop processes every stored index exactly once in its increasing array order, using one exact real multiplication and addition per index.

Proof

1.1givenF2A1induction

The intervals $[r_{i}, r_{i + 1})$ are disjoint and, because $r_{0} = 0$ and $r_{m} = s$ , their union is $[0, s)$ . Thus each stored index has exactly one row $i (t)$ , including the empty-stream case $s = 0$ . After processing the first $k$ stored indices, the accumulator satisfies $w_{j} = \sum_{0 \leq t < k, c_{t} = j} v_{t} y_{i (t)}$ : this holds at $k = 0$ , and the next update adds exactly its one summand to component $c_{k}$ .

2.1F1F2step 1.1algebra

At $k = s$ , for each column $j$ the CSR reconstruction in [F2] gives $(A^{T} y)_{j} = \sum_{i = 0}^{m - 1} A_{i j} y_{i} = \sum_{i = 0}^{m - 1} \sum_{r_{i} \leq t < r_{i + 1}} 1_{c_{t} = j} v_{t} y_{i} = \sum_{0 \leq t < s, c_{t} = j} v_{t} y_{i (t)} = w_{j}$ . The finite row intervals partition the stored indices, so the reindexing counts every stored term once; real multiplication distributes over finite sums. By [F1], $c - w$ is the reduced-cost vector when $y = y (B)$ .

3.1A1step 2.1algebra∎

Each of the $s$ updates performs one multiplication and one addition, and initialization and final subtraction each touch exactly $n$ coordinates. The count follows the stated loop, so duplicate indices and zero-valued entries still contribute one multiplication and one addition each; no timing, bandwidth, or factorization conclusion follows.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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

Dimitris Bertsimas and John N. Tsitsiklis, Introduction to Linear Optimization, §§3.3 and 3.7 (standard reference, not scraped)
Michel Goemans, MIT 18.310 Lecture Notes: Linear Programming, Chapter 3 (standard reference, not scraped)