TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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.

Sylvester's criterion: a real symmetric $n \times n$ matrix with $n \geq 1$ is positive definite if and only if all leading principal minors are positive

Statement

Let $A \in M_{n} (R)$ be symmetric, with $n \geq 1$ , and let $Δ_{k}$ be the determinant of its leading $k \times k$ principal submatrix. Then $A$ is positive definite if and only if

$Δ_{k} > 0 (1 \leq k \leq n) .$

Facts & Assumptions

Given: A real symmetric $n \times n$ matrix $A$ with $n \geq 1$ .

[L1]

Schur block elimination gives $P^{T} M P = A_{0} \oplus S$ and $\det M = \det A_{0} \det S$ when the leading block $A_{0}$ is invertible (For symmetric $M = (\begin{array}{cc} A & B \\ B^{T} & C \end{array})$ with $A$ invertible, a block-unitriangular congruence gives $A \oplus (C - B^{T} A^{- 1} B)$ and factors $\det M$ ).

[L2]

Every real symmetric form is congruent to exactly one matrix $diag (I_{p}, - I_{q}, 0_{r})$ (Sylvester's law of inertia: every real symmetric form is congruent to $diag (I_{p}, - I_{q}, 0_{r})$ , and $(p, q, r)$ is unique).

[L3]

A product of two positive or two negative elements is positive, and multiplication by a positive scalar preserves and reflects strict inequalities (Sign rules for products and monotonicity of multiplication, clauses 1, 3, and 4).

[L4]

A triangular matrix has determinant equal to the product of its diagonal entries, so $\det I_{k} = 1$ (The determinant of a triangular matrix is the product of its diagonal entries).

[L5]

Determinants are multiplicative (For same-sized finite square matrices over a commutative ring, $\det (A B) = \det (A) \det (B)$ ).

[L6]

The determinant of a positive-sized square matrix equals the determinant of its transpose (For every square matrix over a commutative ring, $\det (A^{T}) = \det (A)$ ).

Proof

technique · forward determinant comparison and reverse induction on $n$

1.1

Suppose $A$ is positive definite. Its restriction $A_{k}$ to the first $k$ coordinate subspace is positive definite for every $1 \leq k \leq n$ . In the unique normal form of [L2], a negative or zero diagonal entry would give a nonzero vector of nonpositive value, so the normal form is $I_{k}$ ; choose invertible $P_{k}$ with $P_{k}^{T} A_{k} P_{k} = I_{k}$ . Taking determinants using [L4]–[L6] gives $1 = (\det P_{k})^{2} Δ_{k}$ . Since $\det P_{k} \neq 0$ , its square is positive by [L3], so $Δ_{k} > 0$ .

L2L3L4L5L6givenchoose

1.2

For the converse, the case $n = 1$ reads $A = [Δ_{1}]$ with $Δ_{1} > 0$ , which is positive definite.

basegiven

1.3

Assume $n > 1$ , all $Δ_{k} > 0$ , and the converse in size $n - 1$ . Write $A = (\begin{array}{cc} a & b^{T} \\ b & C \end{array})$ , so $a = Δ_{1} > 0$ , and set $S = C - a^{- 1} b b^{T}$ . For $1 \leq j < n$ , apply [L1] to the leading $(j + 1) \times (j + 1)$ block: $Δ_{j + 1} = a \det S_{j}$ , where $S_{j}$ is the leading $j \times j$ block of $S$ . Thus [L3] gives $\det S_{j} = Δ_{j + 1} / a > 0$ .

ihL1L3given

2.1

The induction hypothesis makes $S$ positive definite. The congruence in [L1] gives $P^{T} A P = [a] \oplus S$ , which is positive definite because $a > 0$ and $S$ is. Since $P$ is invertible, every nonzero vector is $P y$ for a unique nonzero $y$ , so $A$ is positive definite as well.

step 1.3ihL1L3algebra

3.1

Step 1.1 proves the forward implication. Steps 1.2–2.1 prove the reverse implication for every $n \geq 1$ by induction.

step 1.1step 1.2step 2.1discharge-induction∎

Depends on

Used by

Sylvester's criterion verifies positive definiteness for a concrete symmetric 3×3 matrix Example

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 100 results over 20 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

J. Kuan, Positive Definite Matrices (standard reference, not scraped)

Sylvester's criterion: a real symmetric n×nn×n matrix with n≥1n≥1 is positive definite if and only if all leading principal minors are positive