NormalizedGeneration.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Generation persists in the compact normalized family

The word-normalization equations express a fixed vector-space basis as words in the generators. They therefore imply Lie generation for every limiting law.

theorem OAI.PolycyclicRecognition.evalBilinearWord_eq_lieWord line 22
Source documentation
The recursively evaluated operation agrees with the Lie structure that it defines.
```
theorem evalBilinearWord_eq_lieWord (B : V →L[ℝ] V →L[ℝ] V)
    (h : IsLieBracket B) (X : I → V) (w : FreeMagma I) :
    letI := lieRingOfBilinear B h
…
```
Mentions: OAI.PolycyclicRecognition.IsLieBracket, OAI.PolycyclicRecognition.lieRingOfBilinear
theorem OAI.PolycyclicRecognition.lieSpan_eq_top_of_word_basis line 34
Source documentation
Fixed basis-word identities prevent loss of generation in a limit.
```
theorem lieSpan_eq_top_of_word_basis (B : V →L[ℝ] V →L[ℝ] V)
    (h : IsLieBracket B) (X : I → V) (b : Basis J ℝ V) (w : J → FreeMagma I)
    (hw : ∀ j, evalBilinearWord B X (w j) = b j) :
    letI := lieRingOfBilinear B h
…
```
Mentions: OAI.PolycyclicRecognition.IsLieBracket, OAI.PolycyclicRecognition.evalBilinearWord, OAI.PolycyclicRecognition.lieRingOfBilinear