CartanWordModel.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The finite Cartan word model

The support datum uses all ordered bases selected from a finite list that contains every nonzero evaluated word. It is therefore attached to the Lie algebra generators, rather than to an extra family of assumed bases.

structure OAI.PolycyclicRecognition.CartanWordModel line 24
Source documentation
Finite homogeneous generators, their abelianization basis, and an actual lower-central-series bound for the Cartan ideal.
```
structure CartanWordModel where
…
```
theorem OAI.PolycyclicRecognition.nonempty_cartanWordModel line 39
Source documentation
Construction uses the triangular adjoint action and the actual Cartan root ideal; no word-generation or nilpotence premise is left to the caller.
```
theorem nonempty_cartanWordModel {n : ℕ} (T : TriangularAdjoint L n) :
    Nonempty (CartanWordModel H) := by
…
```
Mentions: OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.CartanWordModel
abbrev OAI.PolycyclicRecognition.CartanWordModel.wordList line 50
abbrev OAI.PolycyclicRecognition.CartanWordModel.Bases line 52
instance OAI.PolycyclicRecognition.CartanWordModel.(instance at line 54) line 54
theorem OAI.PolycyclicRecognition.CartanWordModel.mem_wordList_of_eval_ne_zero line 58
Source documentation
No nonzero direction has been omitted by the finite cutoff.
```
theorem mem_wordList_of_eval_ne_zero (w : FreeMagma (Fin M.letterCount))
    (hw : evalBracketWord M.letter w ≠ 0) : w ∈ M.wordList := by
…
```
Mentions: OAI.PolycyclicRecognition.evalBracketWord
theorem OAI.PolycyclicRecognition.CartanWordModel.bracket_mem_wordList line 66
Source documentation
Brackets of list entries are again list entries unless their value is zero.
```
theorem bracket_mem_wordList (u v : FreeMagma (Fin M.letterCount))
    (h : ⁅evalBracketWord M.letter u, evalBracketWord M.letter v⁆ ≠ 0) :
    u * v ∈ M.wordList := M.mem_wordList_of_eval_ne_zero (u * v) h
```
Mentions: OAI.PolycyclicRecognition.evalBracketWord
def OAI.PolycyclicRecognition.CartanWordModel.supportDatum line 71
Source documentation
The finite support data derived from all word bases.
```
def supportDatum {n : ℕ} (T : TriangularAdjoint L n)
    (hunimod : ∀ x : L, LinearMap.trace ℝ L (ad ℝ L x) = 0) :
    SupportDatum (HeightSpace T.character) (Fin M.letterCount) M.Bases :=
…
```
Mentions: OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.SupportDatum, OAI.PolycyclicRecognition.HeightSpace
theorem OAI.PolycyclicRecognition.CartanWordModel.supportDatum_weight line 80
theorem OAI.PolycyclicRecognition.CartanWordModel.segmentSupport_eq_zero_iff line 86
Source documentation
The segment support from the actual finite word model vanishes precisely at zero height. Its other norm properties follow from SupportDatum.normCore.
```
theorem segmentSupport_eq_zero_iff {n : ℕ} (T : TriangularAdjoint L n)
    (hunimod : ∀ x : L, LinearMap.trace ℝ L (ad ℝ L x) = 0)
    (w : HeightSpace T.character) :
    (M.supportDatum T hunimod).segmentSupport w = 0 ↔ w = 0 :=
…
```
Mentions: OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.HeightSpace