TheoremStatement: Literature-sourcedProof: 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.

The strong RRQR swap rule terminates after finitely many swaps

Statement

For a full-column-rank $A \in F^{m \times n}$ , $m \geq n$ , $0 \leq k < n$ , and $f \geq 1$ , run the exact-arithmetic version of Strong rank-revealing QR with finite swaps and explicit statuses. For $k = 0$ the algorithm returns success without swaps. For $1 \leq k < n$ , every accepted swap strictly increases the volume of the selected $k$ columns. Therefore the procedure makes at most $(\binom{n}{k}) - 1$ swaps and returns success if its cap is at least that number. On exact-arithmetic success with $k \geq 1$ , every score is at most $f$ and hence $\max_{i, j} ∣ (R_{11}^{- 1} R_{12})_{i j} ∣ \leq f$ . If a smaller cap is reached while a violation remains, it returns swap-budget-exhausted; a smaller cap can still suffice when the criterion is met earlier.

Facts & Assumptions

Given: A full-column-rank matrix, target $k$ , factor $f \geq 1$ , and the finite-swap procedure.

[F1]

Strong rank-revealing QR with finite swaps and explicit statuses swaps only when the chosen score exceeds $f$ and returns success only when no score exceeds $f$ .

[F2]

A strong RRQR column swap multiplies selected volume by its score: swapping the chosen columns multiplies selected volume by that score.

Proof

1.1F1F2algebra

If $k = 0$ , the algorithm's first branch returns success without a swap. Assume $1 \leq k < n$ . Every accepted swap has score strictly greater than $f \geq 1$ . By [F2] it multiplies the selected volume by a factor strictly greater than one. Thus the selected volume strictly increases at each swap, so no selected subset can recur because its volume is determined by the fixed input matrix and subset.

2.1step 1.1F1algebra

For $1 \leq k < n$ , there are exactly $(\binom{n}{k})$ possible selected $k$ -column subsets. The initial subset has positive volume by full column rank, and by step 1.1 no subset can recur after a strict increase. If $(\binom{n}{k}) - 1$ swaps have occurred, all $(\binom{n}{k})$ subsets have therefore been visited; a remaining violation would prescribe another swap to an already visited subset, contradicting step 1.1. Thus a cap at least $(\binom{n}{k}) - 1$ cannot be reached with a violation remaining, and the algorithm returns success.

3.1F1algebra∎

For $k = 0$ the coefficient assertion is vacuous. For $1 \leq k < n$ , success gives $s_{i j} \leq f$ for all pairs. Since $∣ X_{i j} ∣ \leq s_{i j}$ by the score definition, $\max_{i, j} ∣ X_{i j} ∣ \leq f$ . If a smaller cap is reached while a violation remains, the algorithm returns swap-budget-exhausted; if no violation remains first, it returns success.

Depends on

Used by

Nothing in the library uses this result yet.

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

Ming Gu and Stanley C. Eisenstat, Efficient Algorithms for Computing a Strong Rank-Revealing QR Factorization, §§3–4 (standard reference, not scraped)
Lecture Notes on Matrix Computations, Remark 3.2.2 (standard reference, not scraped)