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.
Scaled real and complex Householder and Givens update arithmetic
Definition
Scalar execution order. These conventions expand every arithmetic expression below into a fixed finite scalar schedule; they do not execute the exact theoretical representatives. Visit vector indices increasingly and matrix columns increasingly, with row indices increasing within each column. Visit the real component before the imaginary component. For a complex vector , its real-component list is . Evaluate displayed assignments in their written order and nested operations from the inside out, left operand before right operand. For inputs and with real components , a complex product uses rounded real products , in that order, followed by the rounded real subtraction and rounded imaginary addition . Do not fuse operations. Return immediately at the first failing primitive; indices refer to this expanded order. Copies, sign changes and conjugations are exact.
For a scaled norm, first form every rounded component divided by the common scale in list order. Then, in that same order, round each component square and accumulate it: copy the first square to the accumulator, and round each subsequent accumulator-plus-square addition. Use this same square-and-sum schedule for the stored-vector squared norm , without scaling. An empty sum is exact zero and requests no primitive. Apply square root and rescaling only at their prescribed subsequent stages. The two-component and four-component norm calls use their displayed component lists in this order.
For the Householder dot row , visit columns increasingly. For each column visit , form the declared complex product , copy the first product as the partial dot, then add each later product by rounded real-component addition followed by rounded imaginary-component addition. Finish all of before forming in increasing row order, then all of in the matrix order above, then all entries of in that order. Evaluate both components of the formation of and every scalar scaling or division in real-then-imaginary order. A separate block call uses already stored and the same stages, omitting formation and target overwrite.
For a Givens application, visit columns increasingly and copy the two old entries before changing either. Compute the upper output first, then the lower output, each by its two products in written order followed by its componentwise addition. Each of the prescribed two complex products uses the six-operation schedule above, including a real coefficient viewed as a complex number with zero imaginary component. Both outputs use the copied old entries. Perform an instructed target zero write only after these outputs. Right applications execute the stated conjugate-transpose reduction with these same conventions. No intermediate is reused across different expressions unless explicitly stored by the procedure.
Use the operationwise real/complex arithmetic model, with six-real-operation complex products and componentwise division by positive real scalars. A scaled norm of a nonzero complex vector first chooses the largest absolute real or imaginary component , rounds every real component divided by , sums their rounded squares sequentially, rounds the positive square root, and rounds multiplication by . A norm of already scaled components omits the last multiplication. Zero input has exact norm zero. Reject every nonzero exact intermediate outside the normal range, nonfinite/invalid operation, and nonpositive required norm; return the first range-failure. All sign changes and conjugations are exact.
For a Householder active block , , a zero copies the block with identity action. Otherwise compute by the scaled norm. If put ; otherwise compute its modulus by its own two-component scaled norm and divide its real and imaginary parts by . Set using real-scalar component multiplication, and . Compute by sequential summation of all rounded real component squares of , and . Compute , , , and . Return , writing exact zeros below the target diagonal, and store . Its theoretical representative is . For a separate block application omit the column overwrite. For a right step apply these instructions to the conjugate-transposed block and transpose back.
For a Givens target pair , use the identity when , including . Otherwise choose as the largest absolute real/imaginary component of , round and componentwise, and compute as the norm of their four already scaled components. If , compute as the norm of its two components, , and . If , set and . Store and apply it to the chosen two rows using two complex products and one rounded componentwise addition for each output entry. For an actual target column, set its intended annihilated entry to exact zero after the update. The initial shift-vector rotation is formed from the shift vector but applied to the matrix without zeroing an unrelated matrix entry. Right applications use the conjugate-transposed form. Its exact unitary representative is ; this normalization defines a mathematical representative and is not an additional rounded operation.
These are arithmetic realizations of the canonical Householder and Givens methods. Returned dense transformation accumulators may be rounded; the exact unitary products used in backward-error statements are represented by the stored local data. Additional discarded matrix entries must be recorded separately, including their magnitudes. Their omission is never implicit in a sparsity convention.
Depends on
Used by
- Finite budget implicit shifted QR for bidiagonal singular values Algorithm
- Finite Householder QR solve for a Padé denominator with explicit statuses Algorithm
- Finite-budget QZ iteration with homogeneous status and residual output Algorithm
- Householder bidiagonalization and its finite precision status Algorithm
- Scaled complex Householder reflector step with explicit range status Algorithm
- Common computed Givens actions certify both pencil matrices and factor residuals Lemma
- Scaled complex Householder and Givens steps have explicit local backward errors Lemma
- The scaled complex Householder wrapper terminates and has a unitary representative on success Lemma
- Finite matrix-function algorithms preserve primitive budgets and terminate with explicit statuses Theorem
- Local stable reflectors and rotations give an aggregate SVD backward error Theorem
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
- Stuart and Voss, Matrix Analysis and Algorithms (standard reference, not scraped)