EvenAlternatingWords.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Under a tracial functional, vanishing of nonempty even alternating centered words implies scalar freeness. The odd-word step rotates the last letter next to the first, centers their product, and shortens the word.

theorem OAI.KadisonSimilarity.AlternatingCenteredWord.take_prefix line 19
Source documentation
Any prefix retains the starting side and centered alternation.
```
theorem take_prefix {side : Bool} {xs ys : List R}
    (h : AlternatingCenteredWord τ P Q side (xs ++ ys)) :
    AlternatingCenteredWord τ P Q side xs := by
…
```
Mentions: OAI.KadisonSimilarity.AlternatingCenteredWord
theorem OAI.KadisonSimilarity.AlternatingCenteredWord.last_mem_of_even_prefix line 29
Source documentation
After an even prefix, the last letter lies in the starting algebra.
```
theorem last_mem_of_even_prefix {side : Bool} (xs : List R) (z : R)
    (h : AlternatingCenteredWord τ P Q side (xs ++ [z]))
    (heven : xs.length % 2 = 0) : z ∈ (if side then P else Q) := by
…
```
Mentions: OAI.KadisonSimilarity.AlternatingCenteredWord

theorem OAI.KadisonSimilarity.AlternatingCenteredWord.append_of_odd_length line 48

Source documentation

Appending the opposite-algebra letter closes an odd alternating word.

theorem append_of_odd_length {side : Bool} (xs : List R) (z : R)
    (h : AlternatingCenteredWord τ P Q side xs)
    (hodd : xs.length % 2 = 1) (hz : z ∈ (if !side then P else Q))
    (hz0 : τ z = 0) :
    AlternatingCenteredWord τ P Q side (xs ++ [z]) := by
…

Mentions: OAI.KadisonSimilarity.AlternatingCenteredWord

theorem OAI.KadisonSimilarity.scalarFree_of_even_alternating line 76
Source documentation
The tracial cyclic reduction needed in the dihedral-corner argument. The only trace identities used are linearity, normalization, and cyclicity.
```
theorem scalarFree_of_even_alternating
    (hτ : τ 1 = 1) (htr : ∀ a b, τ (a * b) = τ (b * a))
    (heven : ∀ side x xs, AlternatingCenteredWord τ P Q side (x :: xs) →
      (x :: xs).length % 2 = 0 → τ ((x :: xs).prod) = 0) :
    ScalarFree τ P Q := by
…
```
Mentions: OAI.KadisonSimilarity.AlternatingCenteredWord, OAI.KadisonSimilarity.ScalarFree
theorem OAI.KadisonSimilarity.scalarFree_of_even_cyclic line 130
Source documentation
It suffices to test even cyclic words beginning in the first algebra; tracial rotation supplies the opposite starting side.
```
theorem scalarFree_of_even_cyclic
    (hτ : τ 1 = 1) (htr : ∀ a b, τ (a * b) = τ (b * a))
    (heven : ∀ x xs, AlternatingCenteredWord τ P Q true (x :: xs) →
      (x :: xs).length % 2 = 0 → τ ((x :: xs).prod) = 0) :
    ScalarFree τ P Q := by
…
```
Mentions: OAI.KadisonSimilarity.AlternatingCenteredWord, OAI.KadisonSimilarity.ScalarFree