Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-31
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 every right-hand side b, A+b is the unique least-squares solution of minimum Euclidean norm

Statement

Let F∈{R,C}, let A∈Mm×n(F), and let b∈Fm. Then A+b is a least-squares solution of Ax=b, and among all least-squares solutions it is the unique one of minimum Euclidean norm.

Facts & Assumptions

Given: A scalar field F∈{R,C}, a matrix A∈Mm×n(F), and a right-hand side b∈Fm.

[L1]

Proof

technique · direct
1.1L1L3L4

By [L1], AA+b is the orthogonal projection of b onto im⁡A. Therefore the residual b−AA+b lies in (im⁡A)⊥=ker⁡A∗ by [L4], so A∗(AA+b−b)=0 and [L3] shows that A+b is a least-squares minimiser.

1.2L2L5algebra

By [L2] and [L5], A+b∈im⁡A+=im⁡A∗=(ker⁡A)⊥. Thus A+b is orthogonal to every vector in ker⁡A.

2.1L3step 1.2algebra

Let x be any least-squares minimiser. By [L3], x−A+b∈ker⁡A, so x=A+b+z for some z∈ker⁡A. Step 1.2 then gives ∥x∥22=∥A+b∥22+∥z∥22≥∥A+b∥22.

3.1step 2.1algebra

Equality in step 2.1 holds only when z=0, so the least-squares minimiser of minimum Euclidean norm is unique and equals A+b.

4.1step 1.1step 2.1step 3.1∎

Step 1.1 proves the least-squares claim and steps 2.1 and 3.1 prove the minimum-norm claim.

Depends on

Used by

Dependency tree · two levels

14 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