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.

Forward and backward substitution are correct, unique, and quadratic in scalar operations

Statement

Let F be a field, let n≥1, and let b∈Fn.

  1. If L∈Mn(F) is lower triangular with nonzero diagonal, the forward substitution recursion of Forward and backward substitution for triangular linear systems produces the unique solution of Lx=b.
  2. If U∈Mn(F) is upper triangular with nonzero diagonal, the backward substitution recursion produces the unique solution of Ux=b.

Each solve uses exactly n divisions, n(n−1)2 multiplications, and n(n−1)2 additions or subtractions, hence O(n2) scalar operations.

Facts & Assumptions

Given: A field F, a natural number n≥1, a vector b∈Fn, and a triangular matrix T∈Mn(F) with nonzero diagonal; when T=L it is lower triangular, and when T=U it is upper triangular.

[L1]

Forward substitution defines xi from the earlier coordinates by xi=ℓii−1(bi−∑j<iℓijxj),and backward substitution defines xi from the later coordinates byxi=uii−1(bi−∑j>iuijxj) (Forward and backward substitution for triangular linear systems).

Proof

technique · induction on the row index, then reverse induction for the upper-triangular case
1.1L1induction

Forward substitution. For i=0, [L1] gives x0=b0/ℓ00, so the first row equation is satisfied. Assume the first i rows are satisfied. Then the (i+1)-st row of a lower-triangular system is ∑j≤i+1ℓi+1,jxj=bi+1, and solving for xi+1 gives exactly the recursion in [L1]. Because ℓi+1,i+1≠0, this value is forced and is unique. Induction proves that the forward recursion solves Lx=b and that no other vector can differ in any coordinate.

1.2L1induction

Backward substitution is the same argument from the last row upward: the last row determines xn−1=bn−1/un−1,n−1, and once xi+1,…,xn−1 are fixed, the i-th row forces xi=uii−1(bi−∑j>iuijxj). Hence the backward recursion solves Ux=b and the solution is unique.

2.1step 1.1step 1.2algebra

In either triangular case, the i-th step forms one sum with i products and i additions in the lower-triangular solve, or with n−1−i products and n−1−i additions in the upper-triangular solve, followed by one division. Summing over all rows gives n divisions and ∑i=0n−1i=∑i=0n−1(n−1−i)=n(n−1)/2 multiplications and the same number of additions.

3.1step 1.1step 1.2step 2.1discharge-induction∎

Step 1.1 proves claim 1, step 1.2 proves claim 2, and step 2.1 gives the operation counts.

Depends on

Used by

Dependency tree · two levels

3 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