FiniteBracketWords.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

A finite list containing every nonzero bracket word

A word of depth k belongs to the kth lower central ideal. Thus a nilpotency bound gives a finite list containing every nonzero evaluated word. The depth cutoff avoids choosing a minimal nilpotence class.

def OAI.PolycyclicRecognition.bracketWordDepth line 22
theorem OAI.PolycyclicRecognition.evalBracketWord_mem_lowerCentralSeries line 26
theorem OAI.PolycyclicRecognition.evalBracketWord_eq_zero_of_depth line 43
def OAI.PolycyclicRecognition.boundedBracketWords line 53
theorem OAI.PolycyclicRecognition.mem_boundedBracketWords line 59
theorem OAI.PolycyclicRecognition.span_boundedBracketWords line 91
Source documentation
Every omitted word evaluates to zero, so this finite list has the same linear span as the set of all words.
```
theorem span_boundedBracketWords (X : I → L) {k : ℕ}
    (hk : lowerCentralSeries ℝ L L k = ⊥) :
    Submodule.span ℝ (evalBracketWord X '' (↑(boundedBracketWords (I := I) k) : Set (FreeMagma I))) =
…
```
Mentions: OAI.PolycyclicRecognition.evalBracketWord, OAI.PolycyclicRecognition.boundedBracketWords
theorem OAI.PolycyclicRecognition.exists_finite_spanning_bracketWords line 107
Source documentation
Nilpotence supplies a finite spanning word list for every finite generating family; no finite-dimensionality assumption is needed for this step.
```
theorem exists_finite_spanning_bracketWords [LieRing.IsNilpotent L]
    (X : I → L) (hX : LieSubalgebra.lieSpan ℝ L (Set.range X) = ⊤) :
    ∃ k : ℕ, Submodule.span ℝ
      (evalBracketWord X '' (↑(boundedBracketWords (I := I) k) : Set (FreeMagma I))) = ⊤ := by
…
```
Mentions: OAI.PolycyclicRecognition.evalBracketWord, OAI.PolycyclicRecognition.boundedBracketWords