Alphabeta Math
CorollaryStatement: 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.

Over a field of characteristic not 2, every symmetric matrix is congruent to a diagonal matrix

Statement

If AMn(F) is symmetric and charF2, then there is an invertible P such that PTAP is diagonal.

Facts & Assumptions

Given: A symmetric matrix AMn(F) over a field of characteristic not 2.

[L2]

Every symmetric bilinear form in the stated characteristic has an orthogonal basis (Every symmetric bilinear form on a finite-dimensional space over a field of characteristic not 2 has an orthogonal basis).

[L3]

A basis change by P sends a bilinear-form matrix A to PTAP (A basis change by P changes the matrix of a bilinear form from A to PTAP).

Proof

technique · direct
1.1

In the standard basis [L1], let B(u,v)=uTAv. Symmetry of A makes B symmetric.

L1givenalgebra
1.2

Choose an orthogonal basis for B by [L2], and let P have those basis vectors as its columns in standard coordinates. Then P is invertible and the matrix of B in that basis is diagonal.

L2choose
2.1

By [L3], this diagonal matrix is PTAP. When n=0, the empty matrix is already diagonal and the same conclusion holds.

step 1.2L3

Depends on

Used by

Dependency tree · next 3 levels

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