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-RRQR interpolative decomposition with explicit statuses
Definition
Input a finite real or complex matrix with , an integer with , a factor , a finite swap cap , and an arithmetic mode: exact arithmetic or finite precision. Finite-precision inputs and the arithmetic format have the represented-dyadic meaning specified by the called QR algorithm; all exact certificate calculations below use unbounded-size rational arithmetic on those represented values. In that mode supply the called QR procedure's finite real format, rounding rule and optional certificate-pass budget (default ); forward them unchanged on the interior call. Its exact unitary is reconstructed from the final sweep's dyadic reflector record, and its score and residual bounds may be symbolic nonnegative square roots of exact rationals. The direct ID check below uses only rational candidate entries and does not require evaluating those square roots. The procedure returns an algorithm status in success, rank-deficient-input, singular-selected-block, swap-budget-exhausted, or range-failure. On a successful branch it returns the selected index list and coefficient matrix ; finite-precision outputs are candidates until their certification status is checked. For , it also returns the RRQR diagnostics specified in step 4, including the rank status, selected-block conditioning data, and score data. In finite precision it returns separately the underlying RRQR certificate status and certificate data, and an ID-certificate status for the returned .
- If , return
success, , and the unique matrix . Then . Set the block, rank, and conditioning diagnostics to not applicable and both certificate statuses tonot-required. This branch includes . - If , return
success, , and . Then . Set the block, rank, and conditioning diagnostics to not applicable and both certificate statuses tonot-required. - If , call Strong rank-revealing QR with finite swaps and explicit statuses on in the requested arithmetic mode. In exact arithmetic, propagate each nonsuccess status without returning . In finite precision, propagate each nonsuccess status, including
range-failure, without returning ; retain any partial diagnostics supplied by the called procedure. On either mode's nonsuccess branch set both certificate statuses tonot-applicableand return no ID-certificate data. - On success, let be the returned column permutation. In exact arithmetic retain the full factorization with unitary and partition its upper-trapezoidal factor after its first rows and columns as In finite precision use the returned candidate factors and the corresponding blocks; the exact unitary transformation representation remains part of the certificate data in step 5. Let be the ordered list of original column indices in the first positions of . Set in exact arithmetic, or use the returned candidate in finite precision, and define by . Retain for the final output , the full factor ( or ), and the diagnostics , where , , and . In finite precision these are candidate values; retain validated enclosures only when supplied by the certificate. Continue to step 5 before returning.
- In exact arithmetic, the returned decomposition and diagnostics refer to the exact successful factorization; set both certificate statuses to
not-required. In finite precision, retain the called procedure's RRQR certificate status and any completed data , including its dyadic reflector record and exact squared quantities, unchanged and independently of the following direct ID check; fields not computed on anuncertifiedbranch remain absent. If a candidate or other required output is nonfinite, returnrange-failurewithout , with both certificate statusesnot-applicable. Otherwise form by copying the candidate entries and inserting exact zeros and ones, so no new rounding changes . For the actual returned , compute in exact rational complex arithmetic Check the dimensions, distinct valid indices in , the entrywise identity , and . Set the ID-certificate status tocertifiedexactly when these checks pass, and otherwise touncertified. Return the exact rational data and the check outcomes in either case. The residual bound is the symbolic nonnegative square root , so its reporting requires no floating-point square root or range conversion. AcertifiedID therefore obeys This direct certificate is independent of the RRQR certificate: it can certify the actual interpolation and this explicit residual bound even when RRQR score certification is unavailable. It does not certify the RRQR singular-value comparison or replace its score and unitary-reconstruction conditions. No iterative certificate search or rounding-based equality test is used. Returnsuccesswith these outputs and the two separately assigned certificate statuses.
The error theorem below concerns exact-arithmetic success. It gives no finite-precision error bound for a returned candidate; a strong singular-value-relative bound additionally requires verified RRQR score and factorization information. Step 5 supplies its separate direct bound for the actual represented output, without asserting that it equals the exact-arithmetic trailing-block bound.
Depends on
Used by
Dependency tree · two levels
4 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)
- Per-Gunnar Martinsson and Joel A. Tropp, Randomized Numerical Linear Algebra: Foundations & Algorithms, §13 (standard reference, not scraped)