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

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

Statement

Let m,nN with n1 and mn, and let AMm×n(R) have full column rank (rank n), with singular values σ1σn>0. Define the spectral condition number of the rectangular matrix A by

κ2(A):=σ1σn;

for a square invertible A this agrees with A2A12 of The condition number kappa_p(A) = ||A||_p ||A^{-1}||_p of a nonsingular linear system. Then:

  1. The normal-equation matrix ATA is invertible, with κ2(ATA)=κ2(A)2;
  2. equivalently, κ2(ATA)=σ12σn2.

The least-squares normal equation ATAx=ATb of For a linear map T:VW between finite-dimensional inner-product spaces, x minimises Txb if and only if T(Txb)=0, equivalently TTx=Tb; minimisers exist and any two differ by an element of kerT therefore has condition number exactly the square of the condition number of the least-squares problem itself.

Facts & Assumptions

Given: A matrix AMm×n(R) of full column rank with n1, mn, and singular values σ1σn>0.

[L1]

There is a singular value decomposition A=UΣVT with orthogonal UMm(R), VMn(R) and Σ diagonal with entries σ1,,σn on the n×n block (Every linear map between finite-dimensional real or complex inner product spaces admits a singular value decomposition).

[L3]

The rank of a linear map is the number of its positive singular values; in particular the full-column-rank hypothesis is exactly σn>0 (The rank of a linear map is the number of its nonzero singular values).

[L4]

Proof

technique · direct
1.1

From [L1], ATA=VΣTΣVT, and ΣTΣ=diag(σ12,,σn2) is diagonal with decreasing nonnegative entries; by [L4], V is orthogonal with VVT=In.

L1L4algebra
2.1

The displayed product Vdiag(σj2)VT is a singular value decomposition of ATA with singular values σ12σn2, since the two orthogonal factors are V and V.

step 1.1L1algebra
3.1

By [L3], full column rank means σn>0, so every singular value of ATA in step 2.1 is positive, and ATA has the inverse Vdiag(σj2)VT: the two products with ATA give In by [L4].

step 2.1L3L4algebra
4.1

By [L2] applied to ATA and to its inverse, ATA2=σ12 and (ATA)12=σn2, the largest singular value of Vdiag(σj2)VT being σn2; hence κ2(ATA)=σ12σn2.

step 2.1step 3.1L2algebra
5.1

By the definition of κ2(A) in the Statement, κ2(A)2=σ12/σn2, which equals the value in step 4.1; this is claim 2, and claim 1 is its equivalence with the condition number of the square invertible matrix ATA from The condition number kappa_p(A) = ||A||_p ||A^{-1}||_p of a nonsingular linear system, the displayed agreement for square A being A12=σn1 by [L2] applied to the SVD A1=VΣ1UT of [L1].

step 4.1L1L2algebra
6.1

The normal equation of [L5] has coefficient matrix ATA, so its condition number is the one computed in step 5.1.

step 5.1L5
7.1

Claims 1 and 2 are step 5.1, and the final sentence is step 6.1.

step 5.1step 6.1

Remarks

  • The square is unavoidable for the normal-equation route. Forming ATA squares the condition number even though the least-squares problem itself has condition number κ2(A); computing with A directly through a QR route keeps the factor κ2(A) instead. For A=(10010800), the Gram-Schmidt factor is R=diag(1,108) while ATA=diag(1,1016).

Depends on

Used by

Dependency tree · two levels

21 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