ModelWordExpansion.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Indexed cuts of actual words in the free diagonal model

The copy positions and the ordered labels are kept separate. Injectivity of the copy positions supplies the off-copy relations, while splitting the finite position list identifies each cut with its actual prefix, middle letter, and suffix.

theorem OAI.KadisonKastler.ofFn_split line 23
def OAI.KadisonKastler.cutPrefixIndex line 28
def OAI.KadisonKastler.cutMiddleIndex line 31
def OAI.KadisonKastler.cutSuffixIndex line 34
theorem OAI.KadisonKastler.ofFn_split_middle line 37
theorem OAI.KadisonKastler.noPreservationCut_ofFn line 48
theorem OAI.KadisonKastler.preservationCut_ofFn line 58
def OAI.KadisonKastler.FreeDiagonalModel.centeredWord line 75
def OAI.KadisonKastler.FreeDiagonalModel.noPreservationWordCut line 78
def OAI.KadisonKastler.FreeDiagonalModel.preservationWordCut line 83

theorem OAI.KadisonKastler.FreeDiagonalModel.centeredWord_eq_cuts line 90

Source documentation

Actual centered words split into their r+1 cuts without preservation and their r cuts with preservation.

theorem centeredWord_eq_cuts {r : ℕ} (position : Fin r → ι)
    (hposition : Function.Injective position) (t : OrderedLabelTuple W r) :
    M.centeredWord W position t =
      (∑ k ∈ range (r + 1), M.noPreservationWordCut W position t k) +
        ∑ k ∈ range r, M.preservationWordCut W position t k := by
…

Mentions: OAI.KadisonKastler.OrderedLabelTuple

theorem OAI.KadisonKastler.FreeDiagonalModel.sum_centeredWord_eq_cuts line 114
theorem OAI.KadisonKastler.FreeDiagonalModel.noPreservationWordCut_eq line 126
Source documentation
The cut before position p is exactly the creation prefix times the annihilation suffix, with their original copy positions.
```
theorem noPreservationWordCut_eq {p q : ℕ} (position : Fin (p + q) → ι)
    (t : OrderedLabelTuple W (p + q)) :
    M.noPreservationWordCut W position t p =
      M.creationWord W (position ∘ Fin.castAdd q) (tupleInitial t) *
        M.annihilationWord W (position ∘ Fin.natAdd p) (tupleFinal t) := by
…
```
Mentions: OAI.KadisonKastler.OrderedLabelTuple, OAI.KadisonKastler.tupleInitial, OAI.KadisonKastler.tupleFinal
theorem OAI.KadisonKastler.FreeDiagonalModel.preservationWordCut_eq line 137
Source documentation
The cut at the distinguished middle position is the creation prefix, the compressed centered projection, and the annihilation suffix.
```
theorem preservationWordCut_eq {p q : ℕ} (position : Fin (p + 1 + q) → ι)
    (t : OrderedLabelTuple W (p + 1 + q)) :
    M.preservationWordCut W position t p =
      M.creationWord W (position ∘ cutPrefixIndex p q) (tupleDropMiddle t).val.1 *
        M.D (position (cutMiddleIndex p q)) (tupleMiddle t) *
          M.annihilationWord W (position ∘ cutSuffixIndex p q) (tupleDropMiddle t).val.2 := by
…
```
Mentions: OAI.KadisonKastler.OrderedLabelTuple, OAI.KadisonKastler.cutPrefixIndex, OAI.KadisonKastler.tupleDropMiddle, OAI.KadisonKastler.cutMiddleIndex, OAI.KadisonKastler.tupleMiddle, OAI.KadisonKastler.cutSuffixIndex
theorem OAI.KadisonKastler.FreeDiagonalModel.sum_noPreservationWordCut_eq line 147
theorem OAI.KadisonKastler.FreeDiagonalModel.sum_preservationWordCut_eq line 156