LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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 Hermitian two-by-two pivot inertia is determined by determinant and trace signs

Statement

Let $D \in C^{2 \times 2}$ be Hermitian, and let $Δ = \det D$ and $t = tr D$ , using the matrix determinant and trace. Here $inertia (D)$ denotes the counts, with multiplicity, of its positive, negative, and zero eigenvalues (Complex Hermitian inertia is invariant under nonsingular congruence). Then $Δ$ and $t$ are real. If $Δ < 0$ , then $inertia (D) = (1, 1, 0)$ . If $Δ > 0$ and $t > 0$ , then $inertia (D) = (2, 0, 0)$ ; if $Δ > 0$ and $t < 0$ , then $inertia (D) = (0, 2, 0)$ . No conclusion is asserted when $Δ = 0$ or when $Δ > 0$ and $t = 0$ .

Facts & Assumptions

Given: A Hermitian matrix $D \in C^{2 \times 2}$ .

[F1]

A Hermitian endomorphism is normal (Self-adjoint and normal endomorphisms of a finite-dimensional real or complex inner product space), and every finite-dimensional complex normal endomorphism has an orthonormal eigenbasis (Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely).

[F2]

Similar matrices have the same characteristic polynomial (Similar matrices have the same characteristic polynomial).

[F3]

The matrix characteristic polynomial is $χ_{D} (x) = \det (x I - D)$ (For $A \in M_{n} (F)$ , the characteristic polynomial is $χ_{A} (x) = \det (x I_{n} - A)$ when $n \geq 1$ , with $χ_{A} (x) = 1$ for the unique $0 \times 0$ matrix).

[F4]

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).

[F5]

For the two-by-two matrix $D$ , the constant coefficient of $χ_{D}$ is $\det D$ and its $x$ coefficient is $- tr D$ ( $χ_{A} (x)$ is monic of degree $n$ ; for $n \geq 1$ its $x^{n - 1}$ coefficient is $- tr (A)$ and its constant coefficient is $(- 1)^{n} \det (A)$ , while $χ_{0 \times 0} = 1$ ).

[F6]

The matrix determinant is the finite Leibniz sum (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix).

[F7]

The matrix trace is the sum of the diagonal entries (The trace $tr (A)$ as the sum of the diagonal entries).

[F8]

Inertia is the triple of positive, negative, and zero eigenvalue counts with multiplicity (Complex Hermitian inertia is invariant under nonsingular congruence).

Proof

1.1givenF1F2F3F4F6choosealgebra

By [F1], choose a unitary $U$ and real eigenvalues $λ_{1}, λ_{2}$ such that $D = U diag (λ_{1}, λ_{2}) U^{*}$ . The matrices $D$ and $diag (λ_{1}, λ_{2})$ are similar, so [F2] gives the same characteristic polynomial. By [F3], [F4] and the determinant definition [F6], $χ_{D} (x) = (x - λ_{1}) (x - λ_{2}) = x^{2} - (λ_{1} + λ_{2}) x + λ_{1} λ_{2}$ .

2.1F5F7step 1.1algebra

By [F5], the constant and linear coefficients of $χ_{D}$ are $Δ$ and $- t$ . The matrix trace is the diagonal sum by [F7]. Comparing with the factorization in step 1.1 gives $Δ = λ_{1} λ_{2}$ and $t = λ_{1} + λ_{2}$ , so both are real.

3.1givenF8step 2.1algebra∎

If $Δ < 0$ , the two real eigenvalues have opposite signs, so there is one positive and one negative eigenvalue. If $Δ > 0$ , their product is positive and neither is zero, so they have the same sign; their sum $t$ is then positive exactly when both are positive and negative exactly when both are negative. By [F8], these sign counts are the three stated inertia triples.

Depends on

Used by

Dependency tree · two levels

33 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

Nicholas J. Higham, Numerical Linear Algebra and Matrix Analysis, MIMS EPrint 2015.103, §5.6 (standard reference, not scraped)