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 law of inertia: every real symmetric form is congruent to , and is unique
Statement
Every symmetric bilinear form on a finite-dimensional real vector space is congruent to exactly one normal form
Equivalently, the numbers of positive, negative, and zero diagonal entries are independent of the diagonalizing basis.
Facts & Assumptions
Given: A symmetric bilinear form on a finite-dimensional real vector space .
Every real symmetric matrix is congruent to a diagonal matrix (Over a field of characteristic not , every symmetric matrix is congruent to a diagonal matrix).
Positive and negative definiteness and the inertia data have the meanings stated for real symmetric forms (Positive and negative definiteness, the inertia , rank , and signature of a real symmetric bilinear or quadratic form).
The constructed real field has the least-upper-bound property and hence is complete ordered (The Cauchy-sequence reals have the least-upper-bound property), so every positive real has a nonzero positive square root (Square roots exist: a unique with ; the positives are ).
For finite-dimensional subspaces , (The dimension formula: for finite-dimensional linear subspaces and of , the subspaces and are finite-dimensional and ).
A subspace of a finite-dimensional -dimensional space has dimension at most (If and is a linear subspace of , then is finite-dimensional, , and if and only if , clause 1).
Rank-nullity gives the dimension of a kernel as ambient dimension minus rank (Rank-nullity: ).
Proof
By [L1], choose a basis in which the matrix is diagonal, say with positive entries , negative entries , and zero entries. For each nonzero , [L3] supplies ; replacing the corresponding basis vector by times it changes to or . This proves existence of the displayed normal form, including and the empty basis when .
In this normal form, the positive coordinate subspace has dimension and the form is positive definite on it. Let be the span of the negative and zero coordinates, of dimension . If a positive-definite subspace had , [L4] and [L5] applied to would give . A nonzero vector there has form value at most , a contradiction. Thus is the intrinsic maximum dimension of a positive-definite subspace.
Applying step 2.1 to shows that is the intrinsic maximum dimension of a negative-definite subspace. The radical is the kernel of the associated map; in normal form its rank is , so [L6] gives its dimension .
Any congruent normal form represents the same bilinear form and therefore has the same two intrinsic maxima and radical dimension. Hence its triple is the same , proving uniqueness.
Steps 1.1 and 4.1 prove existence and uniqueness for all finite dimensions and for degenerate as well as nondegenerate forms.
Depends on
Over a field of characteristic not , every symmetric matrix is congruent to a diagonal matrix
Positive and negative definiteness, the inertia , rank , and signature of a real symmetric bilinear or quadratic form
The Cauchy-sequence reals have the least-upper-bound property
Square roots exist: a unique with ; the positives are
The dimension formula: for finite-dimensional linear subspaces and of , the subspaces and are finite-dimensional and
If and is a linear subspace of , then is finite-dimensional, , and if and only if
Rank-nullity: