Normal-form length in the mod-five Borisov quotient

The base-coordinate trace constructed in GroupUndecidability.Borisov.Mod5.BaseWords is a reduced free-product word: its syllables are nontrivial and alternate between the two cyclic factors. Consequently its displayed length is the canonical free-product normal-form length.

def Undecidability.CoprodIWordLength.singletonWord {ι : Type u_1} {M : ι → Type u_2} [(i : ι) → Monoid (M i)] {i : ι} (m : M i) (hm : m ≠ 1) : Monoid.CoprodI.Word M

The one-letter indexed free-product word.

Equations

• Undecidability.CoprodIWordLength.singletonWord m hm = Monoid.CoprodI.Word.cons m Monoid.CoprodI.Word.empty ⋯ hm

def Undecidability.CoprodIWordLength.twoWord {ι : Type u_1} {M : ι → Type u_2} [(i : ι) → Monoid (M i)] {i j : ι} (hij : i ≠ j) (d : M i) (e : M j) (hd : d ≠ 1) (he : e ≠ 1) : Monoid.CoprodI.Word M

The two-letter indexed free-product word with distinct factor labels.

Equations

• Undecidability.CoprodIWordLength.twoWord hij d e hd he = Monoid.CoprodI.Word.cons d (Undecidability.CoprodIWordLength.singletonWord e he) ⋯ hd

theorem Undecidability.CoprodIWordLength.normalForm_length_mul_of_of_le_two {ι : Type u_1} {M : ι → Type u_2} [(i : ι) → Monoid (M i)] [DecidableEq ι] [(i : ι) → DecidableEq (M i)] {i j : ι} (hij : i ≠ j) (d : M i) (e : M j) : (Monoid.CoprodI.Word.equiv (Monoid.CoprodI.of d * Monoid.CoprodI.of e)).toList.length ≤ 2

A product of two letters from distinct free factors has canonical free-product normal-form length at most two.

theorem Undecidability.BorisovModFiveWordLength.baseLetters_ne_one (rules : Fin 3 → List (Fin 2)) (letters : List BorisovModFiveBaseWords.Basis) (x : BorisovModFiveBaseWords.BaseLetter) : x ∈ BorisovModFiveBaseWords.baseLetters rules letters → x.snd ≠ 1

No base syllable in the displayed trace is the identity of its factor.

theorem Undecidability.BorisovModFiveWordLength.baseLetters_chain_ne (rules : Fin 3 → List (Fin 2)) (letters : List BorisovModFiveBaseWords.Basis) : List.IsChain (fun (x y : BorisovModFiveBaseWords.BaseLetter) => x.fst ≠ y.fst) (BorisovModFiveBaseWords.baseLetters rules letters)

The base trace alternates between the two free factors.

def Undecidability.BorisovModFiveWordLength.baseWord (rules : Fin 3 → List (Fin 2)) (letters : List BorisovModFiveBaseWords.Basis) : Monoid.CoprodI.Word BorisovModFiveBaseWords.Factor5

The displayed base trace, packaged as a reduced free-product word.

Equations

• Undecidability.BorisovModFiveWordLength.baseWord rules letters = { toList := Undecidability.BorisovModFiveBaseWords.baseLetters rules letters, ne_one := ⋯, chain_ne := ⋯ }

@[simp]

theorem Undecidability.BorisovModFiveWordLength.baseWord_prod (rules : Fin 3 → List (Fin 2)) (letters : List BorisovModFiveBaseWords.Basis) : (baseWord rules letters).prod = BorisovModFiveBaseWords.letterProd (BorisovModFiveBaseWords.baseLetters rules letters)

theorem Undecidability.BorisovModFiveWordLength.normalForm_letterProd (rules : Fin 3 → List (Fin 2)) (letters : List BorisovModFiveBaseWords.Basis) : Monoid.CoprodI.Word.equiv (BorisovModFiveBaseWords.letterProd (BorisovModFiveBaseWords.baseLetters rules letters)) = baseWord rules letters

The canonical normal form of the base-coordinate product is exactly the reduced trace constructed above.

theorem Undecidability.BorisovModFiveWordLength.normalForm_letterProd_length (rules : Fin 3 → List (Fin 2)) (letters : List BorisovModFiveBaseWords.Basis) : (Monoid.CoprodI.Word.equiv (BorisovModFiveBaseWords.letterProd (BorisovModFiveBaseWords.baseLetters rules letters))).toList.length = 2 * BorisovModFiveBaseWords.basisRuleCount letters

Every displayed rule letter contributes exactly two syllables to the canonical free-product normal form, while stable letters contribute none.

theorem Undecidability.BorisovModFiveWordLength.normalForm_length_factor_zero_one_le_two (d e : BorisovModFiveQuotient.C5) : (Monoid.CoprodI.Word.equiv (Monoid.CoprodI.of d * Monoid.CoprodI.of e)).toList.length ≤ 2

The concrete two-factor version used for mod-five coefficient words.