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.

Reduced QR over the reals solves full-column-rank least squares without squaring the condition number

Statement

Let AMm×n(R) with mn1 and full column rank. Let

A=Q^R^

be a reduced QR factorisation, with Q^TQ^=In and R^ upper triangular. Then:

  1. The least-squares minimiser of Axb2 is the unique solution of R^x=Q^Tb.
  2. The spectral condition number of R^ equals that of A, whereas the normal-equation matrix satisfies κ2(ATA)=κ2(A)2. Thus the QR route solves with a factor of condition κ2(A) rather than the squared factor κ2(A)2.

Facts & Assumptions

Given: A full-column-rank matrix AMm×n(R), a reduced QR factorisation A=Q^R^, and a vector bRm.

[L1]

Reduced QR factorisation means Q^TQ^=In and R^ upper triangular (Full, reduced, and column-pivoted computational QR factorisations).

[L4]

For full-column-rank A, the normal equations square the spectral condition number (For full-column-rank A, the normal equations square the spectral condition number).

[L5]

Proof

technique · orthogonal decomposition of the residual
1.1

With the reduced QR factorisation supplied by [L2] and shaped as in [L1], extend the columns of Q^ to an orthogonal basis Q=[Q^ Q^]. Then Axb2=QT(Axb)2=(R^xQ^TbQ^Tb)2, so Axb22=R^xQ^Tb22+Q^Tb22. The second term is independent of x, so minimising Axb2 is equivalent to solving R^x=Q^Tb.

L1L2L5algebra
2.1

Because A has full column rank, the upper-triangular factor R^ has nonzero diagonal, so the triangular system of step 1.1 has a unique solution. Thus the least-squares minimiser is unique and equals that solution. This agrees with the normal equation of [L3].

step 1.1L1L3algebra
3.1

Since Q is orthogonal and A=Q(R^0), [L5] implies that A and R^ have the same positive singular values, hence the same spectral condition number. By [L4], the normal-equation matrix has condition number κ2(A)2. Therefore the QR solve uses a factor with condition κ2(A), not the squared condition of the normal equations.

step 2.1L4L5algebra
4.1

Steps 1.1-2.1 prove claim 1, and step 3.1 proves claim 2.

step 1.1step 2.1step 3.1

Depends on

Used by

Dependency tree · two levels

24 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