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.
Permutation matrices, partial pivoting, and the pivot-growth factor
Definition
Let , let or , and let be a permutation of . The corresponding permutation matrix is the matrix whose -th row is the -th row of . Thus left multiplication by permutes the rows of a matrix.
In Gaussian elimination with partial pivoting, ties are resolved by a fixed deterministic rule. At stage one inspects the entries in column from rows through , swaps a row with maximal entry modulus into row , and then eliminates the entries below that pivot.
If is the resulting factorisation, its pivot-growth factor is
provided ; when one declares . The absolute value or modulus is the one from Absolute value in an ordered field on real entries and its standard complex analogue on complex entries.
Depends on
Used by
- Full, reduced, and column-pivoted computational QR factorisations Definition
- A full PLU factorisation can be computed explicitly by hand Example
- Sparse Gaussian elimination can create fill-in in the factors Example
- Every real or complex square matrix admits a PLU factorisation, and the first failed pivot marks the singular boundary Theorem
- In the standard real floating-point model, computed pivoted LU is a nearby factorisation with a pivot-growth dependent backward bound Theorem
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
- Tobin A. Driscoll and Richard J. Braun, Fundamentals of Numerical Computation, Section 2.6 (standard reference, not scraped)
- David Bindel, CS 4220: Numerical Analysis, Blocked LU and Cholesky (standard reference, not scraped)