Free-product syllables in the mod-five Borisov quotient

This file computes the base coordinate of a positive displayed rank-five word in BorisovModFiveQuotient.QuotientGroup. Every rule letter contributes one nontrivial d syllable followed by one nontrivial e syllable. Stable letters change only the inversion parity and hence never remove a syllable.

@[reducible, inline]

abbrev Undecidability.BorisovModFiveBaseWords.Basis : Type

The two stable-generator indices and the three rewriting-rule indices.

Equations

• Undecidability.BorisovModFiveBaseWords.Basis = Undecidability.BorisovCStage.RuleBasis

@[reducible, inline]

abbrev Undecidability.BorisovModFiveBaseWords.Factor5 : Fin 2 → Type

A cyclic group of order five assigned to each base-factor label.

Equations

• Undecidability.BorisovModFiveBaseWords.Factor5 x✝ = Undecidability.BorisovModFiveQuotient.C5

@[reducible, inline]

abbrev Undecidability.BorisovModFiveBaseWords.BaseLetter : Type

A nonidentity base-factor letter paired with its factor label.

Equations

• Undecidability.BorisovModFiveBaseWords.BaseLetter = ((i : Fin 2) × Undecidability.BorisovModFiveBaseWords.Factor5 i)

def Undecidability.BorisovModFiveBaseWords.invertC5 : MulAut BorisovModFiveQuotient.C5

Inversion of the cyclic factor, as an automorphism.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Undecidability.BorisovModFiveBaseWords.invertFactors_pow_of (n : ℕ) (i : Fin 2) (x : BorisovModFiveQuotient.C5) : (BorisovModFiveQuotient.invertFactors ^ n) (Monoid.CoprodI.of x) = Monoid.CoprodI.of ((invertC5 ^ n) x)

def Undecidability.BorisovModFiveBaseWords.twistLetter (n : ℕ) : BaseLetter → BaseLetter

Apply the parity accumulated in n stable letters to one base syllable.

Equations

• Undecidability.BorisovModFiveBaseWords.twistLetter n ⟨i, x_1⟩ = ⟨i, (Undecidability.BorisovModFiveBaseWords.invertC5 ^ n) x_1⟩

@[simp]

theorem Undecidability.BorisovModFiveBaseWords.twistLetter_fst (n : ℕ) (x : BaseLetter) : (twistLetter n x).fst = x.fst

theorem Undecidability.BorisovModFiveBaseWords.twistLetter_ne_one (n : ℕ) (x : BaseLetter) (hx : x.snd ≠ 1) : (twistLetter n x).snd ≠ 1

def Undecidability.BorisovModFiveBaseWords.letterProd (letters : List BaseLetter) : BorisovModFiveQuotient.ModFiveBase

Product of a list of free-product letters.

Equations

• Undecidability.BorisovModFiveBaseWords.letterProd letters = (List.map (fun (x : Undecidability.BorisovModFiveBaseWords.BaseLetter) => Monoid.CoprodI.of x.snd) letters).prod

@[simp]

theorem Undecidability.BorisovModFiveBaseWords.letterProd_cons (x : BaseLetter) (xs : List BaseLetter) : letterProd (x :: xs) = Monoid.CoprodI.of x.snd * letterProd xs

@[simp]

theorem Undecidability.BorisovModFiveBaseWords.letterProd_append (xs ys : List BaseLetter) : letterProd (xs ++ ys) = letterProd xs * letterProd ys

@[simp]

theorem Undecidability.BorisovModFiveBaseWords.invertFactors_pow_letterProd (n : ℕ) (letters : List BaseLetter) : (BorisovModFiveQuotient.invertFactors ^ n) (letterProd letters) = letterProd (List.map (twistLetter n) letters)

def Undecidability.BorisovModFiveBaseWords.stableWeight (rules : Fin 3 → List (Fin 2)) : Basis → ℕ

Stable-letter weight of a displayed basis letter in the source or target system determined by rules.

Equations

• Undecidability.BorisovModFiveBaseWords.stableWeight rules (Sum.inl val) = 1
• Undecidability.BorisovModFiveBaseWords.stableWeight rules (Sum.inr i) = (rules i).length

def Undecidability.BorisovModFiveBaseWords.basisRuleCount : List Basis → ℕ

Number of rule letters in a positive displayed word.

Equations

• Undecidability.BorisovModFiveBaseWords.basisRuleCount [] = 0
• Undecidability.BorisovModFiveBaseWords.basisRuleCount (Sum.inl val :: rest) = Undecidability.BorisovModFiveBaseWords.basisRuleCount rest
• Undecidability.BorisovModFiveBaseWords.basisRuleCount (Sum.inr val :: rest) = Undecidability.BorisovModFiveBaseWords.basisRuleCount rest + 1

def Undecidability.BorisovModFiveBaseWords.rulePair (rules : Fin 3 → List (Fin 2)) (i : Fin 3) : List BaseLetter

The two alternating base syllables contributed by one rule letter.

Equations

• One or more equations did not get rendered due to their size.

def Undecidability.BorisovModFiveBaseWords.baseLetters (rules : Fin 3 → List (Fin 2)) : List Basis → List BaseLetter

Reduced base-syllable trace of the evaluation of a positive displayed word. The tail is twisted by the stable weight of its head.

Equations

• One or more equations did not get rendered due to their size.
• Undecidability.BorisovModFiveBaseWords.baseLetters rules [] = []

@[simp]

theorem Undecidability.BorisovModFiveBaseWords.baseLetters_length (rules : Fin 3 → List (Fin 2)) (letters : List Basis) : (baseLetters rules letters).length = 2 * basisRuleCount letters

def Undecidability.BorisovModFiveBaseWords.quotientBasis (rules : Fin 3 → List (Fin 2)) : Basis → BorisovModFiveQuotient.QuotientGroup

Image in the quotient of one positive displayed basis letter.

Equations

• One or more equations did not get rendered due to their size.
• Undecidability.BorisovModFiveBaseWords.quotientBasis rules (Sum.inl val) = Undecidability.BorisovModFiveQuotient.quotientStable

def Undecidability.BorisovModFiveBaseWords.quotientEval (rules : Fin 3 → List (Fin 2)) (letters : List Basis) : BorisovModFiveQuotient.QuotientGroup

The quotient-group product of the indicated rule-basis letters.

Equations

• Undecidability.BorisovModFiveBaseWords.quotientEval rules letters = (List.map (Undecidability.BorisovModFiveBaseWords.quotientBasis rules) letters).prod

@[simp]

theorem Undecidability.BorisovModFiveBaseWords.quotientStable_pow_left (n : ℕ) : (BorisovModFiveQuotient.quotientStable ^ n).left = 1

@[simp]

theorem Undecidability.BorisovModFiveBaseWords.quotientStable_pow_right (n : ℕ) : (BorisovModFiveQuotient.quotientStable ^ n).right = Multiplicative.ofAdd ↑n

@[simp]

theorem Undecidability.BorisovModFiveBaseWords.quotientBase_left (x : BorisovModFiveQuotient.ModFiveBase) : (BorisovModFiveQuotient.quotientBase x).left = x

@[simp]

theorem Undecidability.BorisovModFiveBaseWords.quotientBase_right (x : BorisovModFiveQuotient.ModFiveBase) : (BorisovModFiveQuotient.quotientBase x).right = 1

@[simp]

theorem Undecidability.BorisovModFiveBaseWords.quotientBase_pow_right (x : BorisovModFiveQuotient.ModFiveBase) (n : ℕ) : (BorisovModFiveQuotient.quotientBase x ^ n).right = 1

@[simp]

theorem Undecidability.BorisovModFiveBaseWords.inversionAction_nat (n : ℕ) : BorisovModFiveQuotient.inversionAction (Multiplicative.ofAdd ↑n) = BorisovModFiveQuotient.invertFactors ^ n

@[simp]

theorem Undecidability.BorisovModFiveBaseWords.invertFactors_pow_modE (n : ℕ) : (BorisovModFiveQuotient.invertFactors ^ n) BorisovModFiveQuotient.modE = Monoid.CoprodI.of ((invertC5 ^ n) BorisovModFiveQuotient.c5Generator)

@[simp]

theorem Undecidability.BorisovModFiveBaseWords.quotientBasis_right (rules : Fin 3 → List (Fin 2)) (q : Basis) : (quotientBasis rules q).right = Multiplicative.ofAdd ↑(stableWeight rules q)

@[simp]

theorem Undecidability.BorisovModFiveBaseWords.quotientBasis_left_stable (rules : Fin 3 → List (Fin 2)) (beta : Fin 2) : (quotientBasis rules (Sum.inl beta)).left = 1

@[simp]

theorem Undecidability.BorisovModFiveBaseWords.quotientBasis_left_rule (rules : Fin 3 → List (Fin 2)) (i : Fin 3) : (quotientBasis rules (Sum.inr i)).left = letterProd (rulePair rules i)

@[simp]

theorem Undecidability.BorisovModFiveBaseWords.quotientEval_left (rules : Fin 3 → List (Fin 2)) (letters : List Basis) : (quotientEval rules letters).left = letterProd (baseLetters rules letters)

Exact base-coordinate evaluation formula.