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.

Every symmetric bilinear form on a finite-dimensional space over a field of characteristic not $2$ has an orthogonal basis

Statement

Let $V$ be finite-dimensional over a field of characteristic not $2$ . Every symmetric bilinear form $B$ on $V$ admits a basis whose distinct vectors are pairwise orthogonal for $B$ .

Facts & Assumptions

Given: A finite-dimensional $F$ -vector space $V$ , $char F \neq 2$ , and a symmetric bilinear form $B$ .

[L1]

In characteristic not $2$ , a symmetric bilinear form is recovered from $q_{B} (v) = B (v, v)$ by $B (u, v) = \frac{1}{2} b_{q_{B}} (u, v)$ (If $char F \neq 2$ , quadratic forms and symmetric bilinear forms correspond by $q (v) = B (v, v)$ and $B (u, v) = \frac{1}{2} b_{q} (u, v)$ ).

[L2]

A subspace of a finite-dimensional space is finite-dimensional, and an independent subset extends without Choice to a basis (If $\dim_{F} V = n$ and $U$ is a linear subspace of $V$ , then $U$ is finite-dimensional, $\dim_{F} U \leq n$ , and $\dim_{F} U = n$ if and only if $U = V$ ).

[L3]

A basis is a linearly independent spanning set; the zero space has the empty basis (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis).

Proof

technique · induction on $n=\dim V$

1.1

If $n = 0$ , the empty basis is orthogonal. If $B = 0$ , any basis is orthogonal.

baseL3given

1.2

Assume $n > 0$ , $B \neq 0$ , and the theorem below dimension $n$ . By [L1], choose $v \in V$ with $B (v, v) \neq 0$ . Put $v^{⊥} = {w : B (w, v) = 0}$ .

ihL1choose

2.1

Every $w \in V$ has the decomposition $w = a v + z$ , where $a = B (w, v) B (v, v)^{- 1}$ and $z = w - a v \in v^{⊥}$ . If $a v \in v^{⊥}$ , then $a B (v, v) = 0$ , so $a = 0$ . Hence $V = F v \oplus v^{⊥}$ .

step 1.2algebra

3.1

Since $v \notin v^{⊥}$ , this subspace is proper and [L2] gives $\dim v^{⊥} < n$ . The restricted form is symmetric, so the induction hypothesis gives it an orthogonal basis; adjoining $v$ gives an orthogonal basis of $V$ .

step 1.2step 2.1ihL2L3

4.1

The base cases and induction step prove the theorem, including degenerate forms and the zero space.

step 1.1step 3.1discharge-induction∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 72 results over 21 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

K. Conrad, Bilinear Forms, §5 (standard reference, not scraped)

Every symmetric bilinear form on a finite-dimensional space over a field of characteristic not 22 has an orthogonal basis