DihedralCornerWords.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

The algebraic even-word step in the dihedral corner argument. Corner letters absorb the reflection on the right, leaving an explicitly alternating centered word in the original free factors.

def OAI.KadisonSimilarity.DihedralCornerWords.pairLetters line 16

Source documentation

The alternating word containing n copies of the pair d,s.

def pairLetters (d s : R) : ℕ → List R
  | 0 => []
  | n + 1 => d :: s :: pairLetters d s n

/-- A positive-power corner block, after absorbing its first reflection. -/

def OAI.KadisonSimilarity.DihedralCornerWords.blockLetters line 21
Source documentation
A positive-power corner block, after absorbing its first reflection.
```
def blockLetters (d s a : R) (l : ℕ) : List R :=
…
```
def OAI.KadisonSimilarity.DihedralCornerWords.productLetters line 25
Source documentation
Concatenate the explicitly alternating expansions of all corner blocks.
```
def productLetters (d s : R) (blocks : List (R × ℕ)) : List R :=
…
```
theorem OAI.KadisonSimilarity.DihedralCornerWords.pairLetters_prod line 31
theorem OAI.KadisonSimilarity.DihedralCornerWords.blockLetters_prod line 39
Source documentation
The corner relation a*d=a is exactly what removes the first d.
```
theorem blockLetters_prod (d s a : R) {l : ℕ} (hl : 0 < l) (had : a * d = a) :
    (blockLetters d s a l).prod = a * (d * s) ^ l := by
…
```
Mentions: OAI.KadisonSimilarity.DihedralCornerWords.blockLetters
theorem OAI.KadisonSimilarity.DihedralCornerWords.productLetters_prod line 47
Source documentation
The concatenated centered word has precisely the original ordered product of corner letters and positive rotation powers.
```
theorem productLetters_prod (d s : R) (blocks : List (R × ℕ))
    (hpositive : ∀ b ∈ blocks, 0 < b.2) (habsorb : ∀ b ∈ blocks, b.1 * d = b.1) :
    (productLetters d s blocks).prod = (blocks.map fun b => b.1 * (d * s) ^ b.2).prod := by
…
```
Mentions: OAI.KadisonSimilarity.DihedralCornerWords.productLetters
theorem OAI.KadisonSimilarity.DihedralCornerWords.product_insert_right_support line 64
Source documentation
Intermediate right support factors disappear because each subsequent letter is left supported on the same idempotent. No idempotence is needed for this purely multiplicative identity.
```
theorem product_insert_right_support (p : R) (xs : List R) (hne : xs ≠ [])
    (hleft : ∀ x ∈ xs, p * x = x) :
    (xs.map fun x => x * p).prod = xs.prod * p := by
…
```
theorem OAI.KadisonSimilarity.DihedralCornerWords.pairLetters_prepend line 93
Source documentation
Prepending any number of d,s pairs preserves the alternating starting side because each such pair has even length.
```
theorem pairLetters_prepend (n : ℕ) (tail : List R)
    (htail : AlternatingCenteredWord τ D A true tail) :
    AlternatingCenteredWord τ D A true (pairLetters d s n ++ tail) := by
…
```
Mentions: OAI.KadisonSimilarity.AlternatingCenteredWord, OAI.KadisonSimilarity.DihedralCornerWords.pairLetters
theorem OAI.KadisonSimilarity.DihedralCornerWords.blockLetters_prepend line 105
Source documentation
A centered corner letter followed by s and rotation pairs is an alternating centered word, ready to concatenate with another block.
```
theorem blockLetters_prepend (a : R) (ha : a ∈ D) (ha0 : τ a = 0)
    (l : ℕ) (tail : List R) (htail : AlternatingCenteredWord τ D A true tail) :
    AlternatingCenteredWord τ D A true (blockLetters d s a l ++ tail) := by
…
```
Mentions: OAI.KadisonSimilarity.AlternatingCenteredWord, OAI.KadisonSimilarity.DihedralCornerWords.blockLetters
theorem OAI.KadisonSimilarity.DihedralCornerWords.productLetters_alternating line 115
Source documentation
The entire expanded corner product is alternating and centered in the original two free algebras.
```
theorem productLetters_alternating (blocks : List (R × ℕ))
    (hmem : ∀ b ∈ blocks, b.1 ∈ D) (hzero : ∀ b ∈ blocks, τ b.1 = 0) :
    AlternatingCenteredWord τ D A true (productLetters d s blocks) := by
…
```
Mentions: OAI.KadisonSimilarity.AlternatingCenteredWord, OAI.KadisonSimilarity.DihedralCornerWords.productLetters
theorem OAI.KadisonSimilarity.DihedralCornerWords.productLetters_ne_nil line 130
Source documentation
A nonempty list of corner blocks produces a nonempty centered word.
```
theorem productLetters_ne_nil {blocks : List (R × ℕ)} (hblocks : blocks ≠ []) :
    productLetters d s blocks ≠ [] := by
…
```
Mentions: OAI.KadisonSimilarity.DihedralCornerWords.productLetters

theorem OAI.KadisonSimilarity.DihedralCornerWords.trace_product_eq_zero line 139

Source documentation

The original algebraic corner-freeness step: every cyclic product of centered corner letters and positive rotation powers has trace zero.

theorem trace_product_eq_zero (hf : ScalarFree τ D A)
    (blocks : List (R × ℕ)) (hblocks : blocks ≠ [])
    (hmem : ∀ b ∈ blocks, b.1 ∈ D) (hzero : ∀ b ∈ blocks, τ b.1 = 0)
    (hpositive : ∀ b ∈ blocks, 0 < b.2) (habsorb : ∀ b ∈ blocks, b.1 * d = b.1) :
    τ ((blocks.map fun b => b.1 * (d * s) ^ b.2).prod) = 0 := by
…

Mentions: OAI.KadisonSimilarity.ScalarFree

theorem OAI.KadisonSimilarity.DihedralCornerWords.trace_product_insert_right_support line 154
Source documentation
For a tracial functional, inserting the common corner support after each letter does not change the trace of a nonempty product.
```
theorem trace_product_insert_right_support
    (htr : ∀ x y, τ (x * y) = τ (y * x)) (p : R)
    (xs : List R) (hne : xs ≠ []) (hleft : ∀ x ∈ xs, p * x = x) :
    τ ((xs.map fun x => x * p).prod) = τ xs.prod := by
…
```

theorem OAI.KadisonSimilarity.DihedralCornerWords.trace_corner_product_eq_zero line 167

Source documentation

The even cyclic trace vanishing remains true with all the actual corner supports inserted.

theorem trace_corner_product_eq_zero (hf : ScalarFree τ D A)
    (htr : ∀ x y, τ (x * y) = τ (y * x)) (p : R)
    (blocks : List (R × ℕ)) (hblocks : blocks ≠ [])
    (hmem : ∀ b ∈ blocks, b.1 ∈ D) (hzero : ∀ b ∈ blocks, τ b.1 = 0)
    (hpositive : ∀ b ∈ blocks, 0 < b.2) (habsorb : ∀ b ∈ blocks, b.1 * d = b.1)
    (hleft : ∀ b ∈ blocks, p * b.1 = b.1) :
    τ ((blocks.map fun b => b.1 * (d * s) ^ b.2 * p).prod) = 0 := by
…

Mentions: OAI.KadisonSimilarity.ScalarFree