split g2: rank 2 and Cartan from b1+b2

Proved

QAlgorithms.Papers.Independent.Gap48.P15.splitG2_b1b2_rank_cartan

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.

Let $L$ be the real matrix Lie algebra generated by BSplitg2 on PDF page 14; $b_i$ denotes its $i$ th displayed matrix. Then

\operatorname{rank}L=2,\qquad (b_1+b_2,\ 2b_4-b_{10}+3b_{11})\text{ is a basis of a Cartan subalgebra of }L.

The starting element $b_1+b_2$ is retained. The rank here is Lie rank; no stronger assertion about the type of this Cartan is added.

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.

/-- Split g2 has rank 2 and Cartan basis [b1+b2,2b4-b10+3b11].
Source: PDF p. 15, RankOfSplitg2[{b1+b2}]. This is Lie rank, not split rank. -/
theorem splitG2_b1b2_rank_cartan :
    LieAlgebra.rank ℝ splitG2 = 2 ∧
    isCartanBasisFor splitG2 ![bSplitG2 0 + bSplitG2 1,
      (2 : ℝ) • bSplitG2 3 - bSplitG2 9 + (3 : ℝ) • bSplitG2 10] := 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. 15, split g2: rank 2 and Cartan from b1+b2

Read-back

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

In $M_8(\mathbb R)$ , with rows and columns numbered $1,\ldots,8$ , let $E_{pq}$ be the matrix unit, and put $J_{pq}=E_{pq}-E_{qp}$ and $Z_{pq}=E_{pq}+E_{qp}$ . Let $L$ be the smallest real vector subspace closed under $[X,Y]=XY-YX$ and containing the matrices

J_{23}-J_{76},\ -J_{42}+J_{68},\ Z_{25}+Z_{47},\ Z_{26}-Z_{48},\ Z_{27}-Z_{45},\ Z_{28}+Z_{46},\ J_{34}+J_{78},\ Z_{35}-Z_{46},\ Z_{36}+Z_{45},\ Z_{37}-Z_{48},\ Z_{38}+Z_{47},\ -J_{65}-J_{78},\ J_{57}+J_{68},\ J_{58}+J_{76}.

The real Lie algebra $L$ has rank $2$ , and there exists a Lie subalgebra $H$ of $L$ that is nilpotent and equals its normalizer in $L$ , such that the ordered pair

\bigl( (J_{23}-J_{76})+(-J_{42}+J_{68}),\ 2(Z_{26}-Z_{48})-(Z_{37}-Z_{48})+3(Z_{38}+Z_{47}) \bigr)

is linearly independent over $\mathbb R$ and has real linear span exactly the image of $H$ in $M_8(\mathbb R)$ .

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