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.
Strong rank-revealing QR with finite swaps and explicit statuses
Definition
Input a real or complex matrix with , a target with , a factor , and a finite swap cap . The exact-arithmetic version is specified below. In finite precision, denotes the represented matrix: each real and imaginary component, and , is a finite binary floating-point number, interpreted as its exact dyadic rational value. The arithmetic format and rounding rule are fixed for a run. A nonfinite input or required rounded intermediate returns range-failure. This mode makes no rank claim about an unspecified matrix before input rounding.
For the finite-precision rank test, copy the represented into exact rational complex arithmetic. Scan columns from left to right with a current pivot row, select the first nonzero entry at or below that row, interchange rows, and eliminate entries below it by exact rational row operations. If no such entry exists, skip that column. Increment the pivot row only after a nonzero pivot. The number of pivots is the reported exact represented-input rank. Return rank-deficient-input if ; otherwise continue with rank status full-column-rank. This test uses unbounded-size rational integers, not the rounded QR diagonal or a numerical-rank threshold. In exact mode, use the same finite row-elimination instructions over the exact input field to decide the rank condition in step 1.
The finite-precision mode additionally takes a finite real binary format containing and closed under sign changes, a fixed rounding rule, and a certificate-pass budget (default ; disables certification). Real and imaginary parts are stored separately. For a real rational result within the format's finite range, returns its specified nearest representable value, with a fixed tie rule, or its specified directed rounding; a result outside that range returns range-failure. Exact zeros are copied as zero. Real addition, subtraction, multiplication, and division mean their exact rational result followed by this rounding; check each divisor before dividing. A real square root of a nonnegative represented number is rounded by comparing that number with squares of the finitely many nonnegative format values: bracket its root, then use the selected directed endpoint or compare with the squared midpoint for nearest rounding. A negative argument or a root beyond the finite range returns range-failure. Thus no exact irrational arithmetic oracle or unbounded precision search is part of this mode. A nonfinite input or any failed required scalar operation immediately returns range-failure with any completed partial data.
Use the following fixed scalar conventions throughout the rounded core. For and , complex addition/subtraction round their two real components; multiplication returns . For division compute with the addition rounded, require , compute the rounded product , and divide its two real components by , rounding each. Conjugation and sign changes are exact copies. For a vector, compute its squared norm by rounding each real-component square and summing them with rounding in increasing coordinate order, real part before imaginary part; apply the rounded nonnegative square root. Dot products use the above rounded complex products and a left-to-right rounded sum. These rules specify every norm and score calculation below; a nonzero vector whose required computed norm is zero returns range-failure.
The initial permutation is , with original labels . A rounded full QR sweep of a fixed current column order starts from , and an empty transformation record. During the initial pivoted sweep, at column compute the rounded norms of for , choose the largest, breaking ties by smallest original column label, and swap the full columns of and their labels. A fixed-order sweep skips these pivot searches. In either sweep, if entrywise, record no transformation and continue. Otherwise copy , compute its rounded norm , and set if ; if , compute its rounded modulus and divide its two components by to form . Set , and for . Compute the rounded squared norm of , require , and put . Record the active index and the exact dyadic components of this nonzero stored before updating anything.
For each column , compute the rounded dot product from the old column, set , then replace each active entry by . For each row of , compute from its old row, set , and replace each active entry by . Finally set to exact zeros by assignment. At the end return , the full candidate , the final permutation and the ordered record. The imposed zeros are part of this rounded procedure, not a claim of exact annihilation; the certificate measures their effect as well as all rounding. There are at most reflector updates per sweep. Empty active tails are skipped, and no norm or quotient is required for them.
In finite precision step 1 uses this pivoted sweep, and step 2 uses a fresh fixed-order sweep on the represented input in its current order. Each fresh sweep resets and its transformation record. Before the triangular solves, decide singularity of its represented by the same exact rational elimination as the input rank test; if singular, return singular-selected-block. Otherwise solve and by rounded back-substitution: for each right-hand-side column, process rows , sum in increasing , subtract from the supplied right-hand side, check the diagonal divisor and use the complex division above. Compute as the rounded norm of row of , as the rounded norm of column of , and as the rounded modulus of . Compute and . Scan these finite candidate lists for the step-4 maxima and its stated tie rules. The diagnostics are rounded candidates, not exact inverse or score identities. For there are no such solves or score lists.
The numbered instructions below specify exact arithmetic; the preceding rounded instructions replace the corresponding factorization, solve and score operations in finite precision.
- If is not full column rank, return
rank-deficient-input. Otherwise initialize a column permutation and the full column-pivoted QR factorization , where is unitary and is upper trapezoidal. At each pivot choose a remaining column of maximal residual -norm, resolving ties by the smallest original column index. Partition after the first rows and columns. Do not return the reduced QR form. The selected first columns then have a nonsingular leading block. For , return this full factorization withsuccess. - For , refactor the current fixed column order in the full QR form, without further pivoting whenever needed, using unitary Householder or Givens transformations. If the selected leading block is singular, return
singular-selected-block. - Form . For let ; for let . Define the swap score .
- If , choose the lexicographically first pair attaining the largest . Otherwise, if , choose the lexicographically first pair attaining the largest score. If neither inequality holds, return
successand the factors, permutation, , and maximum score. The first branch retains the usual coefficient-triggered swap; the second controls the trailing residual needed for the strong spectral comparison. - When a violating pair was chosen, if the swap count is already , return
swap-budget-exhaustedwith the current partial factors. Otherwise interchange the chosen selected and trailing columns in the current permutation. In exact arithmetic restore triangular form with Givens rotations; in finite precision discard the old factors and record, since step 2 recomputes them from in the new fixed order. Increment the swap count and return to step 2.
The statuses are success, rank-deficient-input, singular-selected-block, swap-budget-exhausted, and range-failure. In particular, ordinary column-pivoted QR is only the initialization: the procedure does not assert that its output alone satisfies the strong bounds. Both modes return the full factor shape and available diagnostics. A finite-precision success is a candidate until the following separate certificate is verified. The rounded dense is never asserted to be unitary.
For each recorded active dyadic vector , define the embedded exact rational matrix on its active coordinates, with identity on the preceding coordinates. Its denominator is a strictly positive exact rational. It is exactly unitary: writing gives , and . Thus the ordered sweep record represents the exact unitary product ; an empty record represents . This product corresponds to the final fresh sweep only, and is distinct from the rounded and the nonunitary rounded update coefficients . Its rational representation requires no normalization by an irrational vector norm.
Certification is finite optional postprocessing, independent of the core status. For a nonsuccess status assign not-applicable. On success with , assign uncertified. With perform the following one exact rational pass, using unbounded-size integer numerators and denominators; no retry until success is allowed.
- Check factor dimensions, that is a permutation of , that is exactly upper trapezoidal, and that each recorded vector has the declared active dimension and is nonzero. Reconstruct each by the displayed rational formula, multiply them in the recorded order, and verify entrywise . Any failed check sets
uncertified. - For , apply exact rational elimination to . If singular, the certificate is
uncertified. Otherwise compute its exact inverse by elimination on , normalizing each nonzero pivot and eliminating above and below it. Form and the exact nonnegative rational score squares Set , stored as a symbolic nonnegative square root, and check the rational inequalities for every . These are equivalent to all . They certify the exact scores of the represented blocks, independently of rounded . For this list and every inverse condition are absent. - Compute exactly and . Set , again a symbolic nonnegative square root; then . If all structural and score checks passed, return
certifiedwith the rational record, reconstructed , , , and their check outcomes; otherwise returnuncertifiedwith any completed data. There is no extra residual tolerance implicit in the certificate: its actual residual bound is reported, however large, and any application requiring a small bound must check that separately.
This single finite pass uses at most the prescribed positive pass budget; a supplied certificate is accepted only by recomputing these exact checks. Certification does not change the core status or rounded candidates. It gives precisely a nonsingular when , rigorous combined-score bounds , and an exact unitary representation with the reported reconstruction bound. The bounds concern the represented input ; a claim about different intended data also needs its separately supplied input-error bound. Ordinary rounded score or residual evaluations do not establish this certificate.
Depends on
Used by
- Strong-RRQR interpolative decomposition with explicit statuses Algorithm
- Classical column-pivoted QR can fail the strong coefficient bound Counterexample
- A strong RRQR column swap multiplies selected volume by its score Lemma
- Capped RRQR interpolation returns a status and its direct certificate bounds the actual residual Lemma
- Strong RRQR block singular values compare to the full matrix spectrum Theorem
- Strong-RRQR interpolative decomposition error and coefficient bounds Theorem
- The strong RRQR swap rule terminates after finitely many swaps Theorem
Dependency tree · two levels
11 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)