TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-16

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.

Gram–Schmidt turns every finite independent list into an orthonormal list with the same successive spans

Statement

Let $(v_{0}, \dots, v_{r - 1})$ be a finite linearly independent list in a real or complex inner product space. There is an orthonormal list $(e_{0}, \dots, e_{r - 1})$ such that, for every $k \leq r$ ,

$span (e_{0}, \dots, e_{k - 1}) = span (v_{0}, \dots, v_{k - 1}) .$

It is obtained recursively from

$u_{k} = v_{k} - \sum_{j < k} ⟨ v_{k}, e_{j} ⟩ e_{j}, e_{k} = \frac{u_{k}}{∥ u_{k} ∥} .$

For $r = 0$ , both lists are empty.

Facts & Assumptions

Given: A finite linearly independent list $(v_{0}, \dots, v_{r - 1})$ .

[L1]

An orthonormal list is orthogonal and every listed vector has norm one (Orthogonal vectors and subspaces, orthogonal and orthonormal sets, and orthonormal bases).

[L2]

A finite list $v$ is linearly independent when every list of scalars with $\sum_{i < n} λ_{i} v_{i} = 0_{V}$ has $λ_{i} = 0_{F}$ for all $i < n$ (Linear independence: a finite list $v : n \to V$ is independent when $\sum_{i < n} λ_{i} v_{i} = 0_{V}$ forces every $λ_{i} = 0_{F}$ , and a subset $S \subseteq V$ is independent when every injective finite list into $S$ is independent).

[L3]

For a nonzero vector $u$ , positive definiteness gives $∥ u ∥ > 0$ , so $u / ∥ u ∥$ is defined and has norm one (The norm $∥ v ∥ = \sqrt{⟨ v, v ⟩}$ induced by a real or complex inner product).

[L4]

Every finite orthogonal list of nonzero vectors is linearly independent (Every finite orthogonal list of nonzero vectors is linearly independent).

[L5]

The span of a set is exactly the vectors obtained as finite linear combinations of its elements, including the empty combination. For a finite list, grouping the finitely many terms by their listed vectors gives a coefficient combination indexed by the list. Every subspace containing those vectors contains these combinations. ( $span (S)$ is exactly the set of linear combinations of finite lists of elements of $S$ , and $span (\emptyset) = {0_{V}}$ )

Proof

technique · induction

1.1base

For $r = 0$ there is nothing to construct, and the successive-span assertion at $k = 0$ is equality of zero subspaces.

1.2ihL1algebra

Suppose $e_{0}, \dots, e_{k - 1}$ have been constructed orthonormally with the required span equalities. Define $u_{k}$ by the displayed formula. For $i < k$ , linearity and orthonormality give $⟨ u_{k}, e_{i} ⟩ = ⟨ v_{k}, e_{i} ⟩ - ⟨ v_{k}, e_{i} ⟩ = 0$ .

2.1step 1.2ihL2L3L5

If $u_{k} = 0$ , then $v_{k}$ lies in $span (e_{0}, \dots, e_{k - 1}) = span (v_{0}, \dots, v_{k - 1})$ , say $v_{k} = \sum_{i < k} μ_{i} v_{i}$ ; then the scalars $λ_{i} = μ_{i}$ for $i < k$ , $λ_{k} = - 1_{F}$ and $λ_{i} = 0_{F}$ for $i > k$ satisfy $\sum_{i} λ_{i} v_{i} = 0_{V}$ with $λ_{k} \neq 0_{F}$ , contradicting the independence of $v$ through [L2]. Hence $u_{k} \neq 0$ , and [L3] makes $e_{k} = u_{k} / ∥ u_{k} ∥$ a unit vector orthogonal to its predecessors.

3.1step 2.1ihL5algebra

The formula for $u_{k}$ shows $e_{k}$ lies in $span (v_{0}, \dots, v_{k})$ , while its rearrangement shows $v_{k}$ lies in $span (e_{0}, \dots, e_{k})$ . Together with the induction hypothesis these give both inclusions in the span equality at $k + 1$ .

4.1step 1.1step 1.2step 2.1step 3.1L1L4discharge-induction∎

Induction constructs the stated list and proves every successive-span equality. Its vectors are nonzero and orthogonal, so [L4] also confirms their independence; their unit norms make the list orthonormal.

Gram–Schmidt turns every finite independent list into an orthonormal list with the same successive spans

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources