claimstandardinferred_dep

Nonalternating binary spaces have orthonormal bases

Nondegenerate nonalternating spaces over F2\mathbb F_2 have orthonormal bases
supplies the orthonormal bases for residuals
Claim·§3.3 Subspaces attached to the gates·inside lemEdge residuals and rank budget

Statement (paper)

Every nondegenerate nonalternating symmetric bilinear space over F2\mathbb F_2 has an orthonormal basis.

In plain English

Every nondegenerate symmetric bilinear space over F2\mathbb F_2 that is not alternating (some vector vv has ⟨v,v⟩=1\langle v,v\rangle=1) has an orthonormal basis.

Why it's here

This is the standard linear-algebra fact that finishes the parent lemma. Combined with the previous claim, which shows nonzero binary residuals are nondegenerate and nonalternating, it gives an orthonormal basis for every nonzero orthogonal residual of an edge.
Classified standard:
Classical classification of symmetric bilinear forms over fields of characteristic 2: a nondegenerate non-alternating symmetric form is diagonalizable with an orthonormal basis (e.g. Albert 1938; Milnor–Husemoller, Symmetric Bilinear Forms).

Uses

claimNonzero binary residuals are nonalternating

Used by

Nothing in the paper

Sources

PaperOpen
Section
§3.3 Subspaces attached to the gates
Page
—
Label
—
Line
sections/03-motifs.tex:441
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Nonalternating binary spaces have orthonormal bases" rests on claim-lem-motif-residuals-3