so(n): BSo ordered basis

Proved

QAlgorithms.Papers.Independent.Gap48.P15.so_ordered_basis

by Goku · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

All matrices and spans are over $\mathbb R$ , and the Lie bracket is $[X,Y]=XY-YX$ . The source uses one-based matrix indices. Write $F_{pq}$ for the matrix unit, $J_{pq}=F_{pq}-F_{qp}$ and $Z_{pq}=F_{pq}+F_{qp}$ . Here rank means Lie rank, and a Cartan subalgebra means a nilpotent, self-normalizing Lie subalgebra.

For every integer $t\ge1$ , let $\mathfrak{so}(t,\mathbb R)=\{X:X^{\mathsf T}=-X\}$ . Enumerate $J_{pq}$ by increasing $p=1,\ldots,t-1$ and then increasing $q=p+1,\ldots,t$ , obtaining the ordered family $B_{\rm So}(t)$ . Then

|B_{\rm So}(t)|=\frac{t(t-1)}2,\qquad B_{\rm So}(t)\text{ is a real basis of }\mathfrak{so}(t,\mathbb R).

For $t=1$ this is the empty basis of the zero Lie algebra.

The explicit family is asserted to be linearly independent and to span the indicated subalgebra; these properties are conclusions. This records the mathematical assertion accompanying the source output.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Gap48_P15

Formal statement

namespace QAlgorithms.Papers.Independent.Gap48.P15

attribute [local instance 100] LieRing.ofAssociativeRing

-- Reuse Mathlib Matrix and Matrix.single directly. Natural one-based
-- coordinates are restricted to Fin coordinates with Matrix.submatrix.

/-- BSo is an ordered real basis of so(t), including its stated cardinality.
Source: PDF p. 5, BSo. The positive-size convention includes t=1 and its empty basis. -/
theorem so_ordered_basis (t : ℕ) (ht : 0 < t) :
    (bSo t).length = t * (t - 1) / 2 ∧
    isBasisFor (LieAlgebra.Orthogonal.so (Fin t) ℝ) (listFamily (bSo t)) := by sorry

end QAlgorithms.Papers.Independent.Gap48.P15

Source

Algorithm to compute the rank and a Cartan subalgebra of a matrix Lie algebra with Mathematica, arXiv:math/0205235v1, PDF p. 5, so(n): BSo ordered basis

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For every natural number $t>0$ , let $E_{pq}$ denote the real $t\times t$ matrix with a single $1$ in row $p$ , column $q$ , using labels $1,\ldots,t$ , and zeros elsewhere. Form the ordered list of matrices $E_{pq}-E_{qp}$ by taking $p=1,\ldots,t$ in increasing order and, for each $p$ , taking $q=p+1,\ldots,t$ in increasing order. This list has length $t(t-1)/2$ , and the family obtained by indexing its entries from zero is linearly independent over $\mathbb R$ and has real linear span equal to the space

\mathfrak{so}(t,\mathbb R)=\{A\in M_t(\mathbb R):A^{\mathsf T}=-A\}.

In particular, $t=1$ is included: the list is empty and its span is the zero space; $t=0$ is excluded by the hypothesis.

Human review

Endorsed by Shuze Chen · Oct 21, 2026
Confirmed by the moderator at approval.
Endorsed by Goku · Oct 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph