compact g2: rank 2 and Cartan from b1+5b5

Proved

QAlgorithms.Papers.Independent.Gap48.P15.compactG2_mixed_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 the literal compact Bg2 family on PDF page 12; $b_i$ denotes its $i$ th displayed matrix. Then

\operatorname{rank}L=2,\qquad (b_1+5b_5,b_1+5b_9)\text{ is a basis of a Cartan subalgebra of }L.

This is the second page-14 output, extending the starting element $b_1+5b_5$ . Both occurrences of $b_1$ and both factors $5$ are retained.

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.

/-- Compact g2 has rank 2 and the distinct Cartan basis [b1+5b5,b1+5b9].
Source: PDF p. 14, second RankOfg2 output. -/
theorem compactG2_mixed_rank_cartan :
    LieAlgebra.rank ℝ compactG2 = 2 ∧
    isCartanBasisFor compactG2 ![bG2 0 + (5 : ℝ) • bG2 4,
      bG2 0 + (5 : ℝ) • bG2 8] := 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. 14, compact g2: rank 2 and Cartan from b1+5b5

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}$ . Let $L$ be the smallest real vector subspace closed under $[X,Y]=XY-YX$ and containing the matrices

J_{23}+J_{67},\ J_{24}+J_{68},\ J_{25}+J_{74},\ J_{26}+J_{84},\ J_{27}+J_{45},\ J_{28}+J_{46},\ J_{34}+J_{78},\ J_{35}+J_{46},\ J_{36}+J_{54},\ J_{37}+J_{84},\ J_{38}+J_{47},\ J_{56}+J_{78},\ J_{57}+J_{86},\ J_{58}+J_{67}.

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_{67}+5(J_{27}+J_{45}),\ J_{23}+J_{67}+5(J_{36}+J_{54}) \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