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.

A matrix admits a Cholesky factorisation with positive diagonal exactly when it is Hermitian positive definite, and that factor is unique

Statement

Let n≥1 and let A∈Mn(C), with the real case obtained by restricting scalars to R. Then the following are equivalent:

  1. A has a Cholesky factorisation A=LL∗ with L lower triangular and positive real diagonal.
  2. A is Hermitian positive definite.

When these conditions hold, the factor L is unique.

Facts & Assumptions

Given: A matrix A∈Mn(C).

[L1]

Hermitian positive-definite matrices and Cholesky factorisations with positive diagonal are defined in Hermitian positive-definite matrices and Cholesky factorisation A = LL* with positive diagonal.

[L2]

The determinant of a triangular matrix is the product of its diagonal entries (The determinant of a triangular matrix is the product of its diagonal entries).

Proof

technique · block induction with a quotient comparison for uniqueness
1.1L1L2L3L4algebra

Suppose A=LL∗ as in [L1]. Then A∗=LL∗=A, so A is Hermitian. For any nonzero x, one has x∗Ax=x∗LL∗x=(L∗x)∗(L∗x)=∥L∗x∥22. The diagonal of L is positive, hence nonzero; [L2] and [L3] give det⁡L≠0, so L is invertible and L∗x≠0 when x≠0. Therefore x∗Ax>0.

1.2baseL1algebra

For the converse, use induction on n. The case n=1 is immediate: A=[a] is Hermitian positive definite exactly when a>0, in which case A=[a][a]∗.

1.3ihL1algebra

Assume n>1 and the converse for size n−1. Write A=(ar∗rC). Positive definiteness of A at x=e0 gives a>0. Set ℓ:=r/a and S:=C−ℓℓ∗. For nonzero y∈Cn−1, apply positive definiteness to x=(−a−1r∗yy): 0<x∗Ax=y∗Sy. Thus S is Hermitian positive definite. By the induction hypothesis, S=L~L~∗ with L~ lower triangular and positive diagonal.

2.1step 1.3L1L4algebra

Define L:=(a0ℓL~). Direct multiplication gives LL∗=(ar∗rℓℓ∗+L~L~∗)=(ar∗rC)=A. The matrix L is lower triangular and its diagonal is positive real, so this is a Cholesky factorisation.

3.1step 1.1step 2.1L2L3algebra

For uniqueness, suppose A=L1L1∗=L2L2∗ are two such factorizations. Then M:=L2−1L1 is lower triangular, and MM∗=I because L2MM∗L2∗=L1L1∗=L2L2∗. A lower-triangular unitary matrix has zero strict-lower entries and diagonal entries of modulus 1; since the diagonal of M is the ratio of two positive real diagonals, each diagonal entry is also positive real, hence equals 1. Therefore M=I and L1=L2.

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

Step 1.1 proves that a Cholesky factorisation implies Hermitian positive definiteness. Steps 1.2-2.1 prove the converse by induction, and step 3.1 gives uniqueness.

Depends on

Used by

Dependency tree · two levels

13 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