sl(n): Bsl ordered basis

Proved

QAlgorithms.Papers.Independent.Gap48.P15.sl_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{sl}(t,\mathbb R)=\{X:\operatorname{tr}X=0\}$ . Let $B_{\rm sl}(t)$ list all $F_{pq}$ with $p\ne q$ in increasing row then column order, followed by $F_{11}-F_{pp}$ for $p=2,\ldots,t$ . Then

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

For $t=1$ the family is empty and the Lie algebra is zero.

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.

/-- Bsl is an ordered real basis of sl(t), with t^2-1 elements.
Source: PDF pp. 9-10. The positive-size convention includes t=1 and its empty basis. -/
theorem sl_ordered_basis (t : ℕ) (ht : 0 < t) :
    (bSl t).length = t ^ 2 - 1 ∧
    isBasisFor (LieAlgebra.SpecialLinear.sl (Fin t) ℝ) (listFamily (bSl 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. 9, sl(n): Bsl 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 an ordered list by first listing $E_{pq}$ with $p=1,\ldots,t$ in increasing order and, for each $p$ , $q=1,\ldots,t$ in increasing order with $q\ne p$ , and then appending

E_{11}-E_{22},\ E_{11}-E_{33},\ \ldots,\ E_{11}-E_{tt}.

This list has length $t^2-1$ , and the family obtained by indexing its entries from zero is linearly independent over $\mathbb R$ and has real linear span equal to

\mathfrak{sl}(t,\mathbb R)=\{A\in M_t(\mathbb R):\operatorname{tr}(A)=0\}.

The case $t=1$ is included: both portions of the list are empty and their 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