PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.ShirshovWords

For any two alternating-block words $w_1$ and $w_2$ (represented as the type `BWord`), if their sequences of blocks $w_1.\text{blocks}$ and $w_2.\text{blocks}$ are equal, then the words $w_1$ and $w_2$ are equal. Here, the block list is the alternating sequence of letters and their positive multiplicities that uniquely defines the word.

For a word $w$ represented as an alternating sequence of blocks (maximal runs of the same letter), its height is defined as the total number of these blocks. For instance, a word such as $a^{n_1}b^{m_1}a^{n_2}b^{m_2}\dots$ has a height equal to the number of terms in the sequence of its constituent blocks.

For a word $w$ represented as a sequence of alternating blocks $(l_i, m_i)$ (where each $l_i$ is a letter and $m_i$ is its positive multiplicity), the degree of $w$ is the sum of the multiplicities of all its blocks, $\sum m_i$. This value represents the total length of the word as a string of letters.

Given a letter $d \in \{0, 1\}$ and a positive natural number $m$, the function constructs a word consisting of a single block of $m$ copies of the letter $d$. This results in a word of height 1, represented by the block list $[(d, m)]$, corresponding to the associative word $d^m$.

For any letter $d \in \{0, 1\}$ and any positive natural number $m$, the list of blocks representing the single-run word $d^m$ (constructed via `ofRun`) is exactly the singleton list containing the pair $(d, m)$.

For any letter $d \in \{0, 1\}$ and any positive natural number $m > 0$, the height of the word consisting of a single block of $m$ copies of the letter $d$ (denoted $d^m$) is equal to $1$.

The type $\text{BWord}$, which represents words in two letters as alternating lists of blocks, is an inhabited type. Its default instance is the empty word, which is represented by an empty list of blocks $[ ]$ and has a height of $0$ and a degree of $0$.

The function `consMerge` takes a letter $d \in \text{Fin } 2$, a positive multiplicity $m \in \mathbb{N}$, and a list $L$ of blocks (where each block is a pair consisting of a letter and its multiplicity). It prepends the block $(d, m)$ to the list $L$ with the following logic: - If $L$ is empty, it returns the list containing only the block $[(d, m)]$. - If $L$ starts with a block $(d', m')$, and $d = d'$, it merges the two blocks into a single block with the same letter and the sum of the multiplicities, returning $(d, m + m') :: \text{tail}(L)$. - If $L$ starts with a block $(d', m')$, and $d \neq d'$, it simply prepends the new block to the list, returning $(d, m) :: L$.

Let $d \in \text{Fin } 2$ be a letter and $m$ be a positive natural number. Let $L$ be a list of blocks, where each block is a pair consisting of a letter and a multiplicity. If $L$ satisfies the condition that any two adjacent blocks have distinct letters, then the list resulting from prepending and merging the block $(d, m)$ into $L$ (using `consMerge`) also satisfies the condition that any two adjacent blocks have distinct letters.

Let $d \in \text{Fin } 2$ be a letter and $m$ be a positive natural number ($m > 0$). Let $L$ be a list of blocks, where each block $p$ is a pair consisting of a letter and a multiplicity $p.2 \in \mathbb{N}$. If every block $p \in L$ has a positive multiplicity ($p.2 > 0$), then every block $q$ in the list produced by prepending and merging the block $(d, m)$ into $L$ (using `consMerge`) also has a positive multiplicity ($q.2 > 0$).

Let $w$ be a block word ($BWord$), which is represented as a list of blocks where each block $p$ consists of a letter and a multiplicity $p.2 \in \mathbb{N}$. For every block $p$ in the list $w.\text{blocks}.\text{dropLast}$ (the list of blocks of $w$ excluding the last one), the multiplicity $p.2$ is strictly positive ($p.2 > 0$).

For any `BWord` $w$, the list of blocks obtained by removing the last element, denoted as `w.blocks.dropLast`, remains alternating. That is, for any two consecutive blocks $p$ and $q$ in the shortened list, the letters (the first components of the pairs) are distinct: $p.1 \neq q.1$.

Given an alternating-block word $w$ represented as a list of $k$ blocks $[(d_1, m_1), (d_2, m_2), \dots, (d_k, m_k)]$, where each block consists of a letter $d_i \in \{0, 1\}$ and a positive multiplicity $m_i \in \mathbb{N}$, Shirshov's reduction map $\alpha \mapsto \bar{\alpha}$ (denoted here as `bar w`) is defined as follows: - If the height $k$ of the word is less than or equal to 1, then $\bar{w} = w$. - If $k > 1$, the trailing block $(d_k, m_k)$ is removed from the end and moved to the front of the remaining sequence $[(d_1, m_1), \dots, (d_{k-1}, m_{k-1})]$. - If the letter of the trailing block matches the letter of the first block (i.e., $d_k = d_1$), the two are merged into a single block with multiplicity $m_k + m_1$. - Otherwise, $(d_k, m_k)$ is prepended as a new distinct block. This map is non-increasing on the height of the word and strictly height-decreasing for words of height $k \ge 3$, making it suitable as a recursion measure. Note that this operation is not an involution and does not correspond to a full reversal of the word.

For any alternating-block word $w$, if its height (the number of blocks in its representation, denoted as `w.blocks.length`) is less than or equal to 1, then Shirshov's reduction map $\bar{w}$ (denoted as `bar w`) is equal to $w$.

For any letter $d \in \text{Fin } 2$, any positive multiplicity $m \in \mathbb{N}$ (where $m > 0$), and any list $L$ of blocks (where each block is a pair consisting of a letter and its multiplicity), the length of the list resulting from prepending and potentially merging the block $(d, m)$ into $L$ via the `consMerge` operation is at most the length of $L$ plus one. That is, $$\text{length}(\text{consMerge}(d, m, L)) \le \text{length}(L) + 1.$$ The `consMerge` function prepends the block $(d, m)$ as a new element if $L$ is empty or if its first block has a different letter than $d$; otherwise, it merges $(d, m)$ into the first block of $L$ by adding the multiplicities, which preserves the list length.

Let $w$ be an alternating-block word in two letters, and let $\text{height}(w)$ denote the number of its constituent blocks (maximal runs of the same letter). Let $\bar{w}$ denote Shirshov's reduction of $w$, which is obtained by moving the trailing block to the front and merging it with the original first block if they share the same letter. Then the height of the reduced word is less than or equal to the height of the original word: $$\text{height}(\bar{w}) \le \text{height}(w).$$