DihedralWordOrthogonality.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Orthogonality of the actual dihedral word inclusions

Alternating-centered-word freeness computes the tracial pairing of the words e (s d)^k a. The algebraic calculation only needs e in the first free algebra; its projection and support properties enter when these pairings are used to construct the normalized Hilbert-space inclusions.

def OAI.KadisonSimilarity.dihedralPairs line 19
theorem OAI.KadisonSimilarity.dihedralPairs_prod line 24
def OAI.KadisonSimilarity.dihedralSandwich line 30
theorem OAI.KadisonSimilarity.dihedralSandwich_prod line 35
theorem OAI.KadisonSimilarity.dihedralPairs_left_alternating line 48
theorem OAI.KadisonSimilarity.dihedralPairs_right_alternating line 55
theorem OAI.KadisonSimilarity.dihedralSandwich_alternating line 62
theorem OAI.KadisonSimilarity.trace_nonempty_alternating line 69
theorem OAI.KadisonSimilarity.dihedralPairs_append_alternating line 75

theorem OAI.KadisonSimilarity.trace_test_dihedral_power line 84

Source documentation

Every positive residual dihedral power pairs trivially with the entire second algebra, from either orientation.

theorem trace_test_dihedral_power (htr : ∀ a b, τ (a * b) = τ (b * a))
    {a : R} (ha : a ∈ Q) {n : ℕ} (hn : 0 < n) :
    τ (a * (d * s) ^ n) = 0 ∧ τ (a * (s * d) ^ n) = 0 := by
…

theorem OAI.KadisonSimilarity.trace_centered_dihedral_sandwich line 109
Source documentation
A centered first-algebra letter between the two dihedral halves has zero trace against every second-algebra coefficient.
```
theorem trace_centered_dihedral_sandwich {e a : R} (he : e ∈ P) (he0 : τ e = 0)
    (ha : a ∈ Q) (k j : ℕ) : τ (a * ((d * s) ^ k * e * (s * d) ^ j)) = 0 := by
…
```
theorem OAI.KadisonSimilarity.dihedral_cancel_successors line 124
theorem OAI.KadisonSimilarity.trace_test_dihedral_product line 131

theorem OAI.KadisonSimilarity.trace_dihedral_sandwich line 151

Source documentation

The scalar trace of the middle letter is the only surviving contribution to the diagonal word pairing.

theorem trace_dihedral_sandwich (htr : ∀ a b, τ (a * b) = τ (b * a))
    (hdd : d * d = 1) (hss : s * s = 1) {e a : R} (he : e ∈ P) (ha : a ∈ Q)
    (k j : ℕ) :
    τ (a * ((d * s) ^ k * e * (s * d) ^ j)) = if k = j then τ e * τ a else 0 := by
…

theorem OAI.KadisonSimilarity.dihedral_word_pairing line 170

Source documentation

The exact inner-product identity for the unnormalized word maps v ↦ e (s d)^k v. No projection or support hypothesis on e is needed for this tracial sandwich identity.

theorem dihedral_word_pairing (htr : ∀ a b, τ (a * b) = τ (b * a))
    (hdd : d * d = 1) (hss : s * s = 1) {e v w : R}
    (he : e ∈ P) (hv : v ∈ Q) (hw : w ∈ Q) (k j : ℕ) :
    τ (star v * (d * s) ^ k * e * (s * d) ^ j * w) =
      if k = j then τ e * τ (star v * w) else 0 := by
…