CartanWordTrace.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Balanced letter counts for actual Cartan word bases

The trace calculation is valid for generalized roots: no diagonalizability or triangularity of the chosen word basis is assumed.

theorem OAI.PolycyclicRecognition.cartan_word_mem_genWeight line 27

theorem OAI.PolycyclicRecognition.trace_cartan_word_basis line 54

Source documentation

The trace character on the ideal is the sum of the actual letter weights, counted with their occurrences in the selected word basis.

theorem trace_cartan_word_basis {J : Type*} [Fintype J]
    (b : Basis J ℝ (cartanRootIdeal H)) (words : J → FreeMagma I)
    (hwords : ∀ j, evalBracketWord X (words j) = b j) (h : H) :
    LinearMap.trace ℝ (cartanRootIdeal H) (toEnd ℝ H (cartanRootIdeal H) h) =
      ∑ i, ((∑ j, bracketWordCount (words j) i : ℕ) : ℝ) * χ i h := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.evalBracketWord, OAI.PolycyclicRecognition.bracketWordCount

theorem OAI.PolycyclicRecognition.balanced_cartan_word_counts line 80