Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-08-30
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.

Successive Householder or Givens transformations produce full and reduced QR factorisations with the standard dense operation counts

Statement

Let AMm×n(F) with F=R or C and mn.

  1. Successive Householder reflectors or Givens transformations can zero the subdiagonal entries column by column and produce a full QR factorisation A=QR and hence a reduced QR factorisation A=Q^R^.
  2. In dense real arithmetic, Householder QR uses 2mn223n3+O(mn) scalar operations, while dense Givens QR uses 3mn2n3+O(mn) scalar operations.

Facts & Assumptions

Given: A matrix AMm×n(F) with mn.

[L1]

Full and reduced computational QR factorisations are defined in Full, reduced, and column-pivoted computational QR factorisations.

[L2]

Householder reflectors and Givens transformations are orthogonal or unitary and can annihilate chosen entries below the diagonal (Householder reflectors and Givens transformations are unitary and can annihilate prescribed entries).

Proof

technique · induction on the column index and summation of the shrinking trailing updates
1.1

For column k, apply [L2] to the subvector of rows k through m1. Embedding the resulting reflector or sequence of Givens transformations into the identity on the first k rows leaves the earlier zeros unchanged and zeros all entries below the diagonal in column k. Repeating for k=0,,n1 produces a unitary matrix Q whose product with A is upper trapezoidal; therefore A=QR with Q=(Q), and deleting the zero rows of R gives the reduced factorisation, in the computational form refining the abstract QR existence of [L3].

L1L2L3induction
2.1

In a dense real Householder step on the trailing block of size (mk)×(nk), forming the reflector costs O(mk) scalar operations and applying it to the trailing block costs 4(mk)(nk) scalar operations. Summing over k=0,,n1 gives 4k=0n1(mk)(nk)+O ⁣(k=0n1(mk))=2mn223n3+O(mn).

step 1.1algebra
2.2

In dense real Givens QR, column k has mk1 entries to eliminate below the diagonal, and each rotation updates two rows across the remaining nk columns using 6(nk)+O(1) scalar operations. Hence the cost is 6k=0n1(mk1)(nk)+O(mn)=3mn2n3+O(mn).

step 1.1algebra
3.1

Step 1.1 proves the constructive QR statement, and steps 2.1-2.2 give the standard dense operation counts.

step 1.1step 2.1step 2.2discharge-induction

Depends on

Used by

Dependency tree · two levels

13 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