RightNormalForm

Part of the dependency closure of the small undecidable group constructions.

@[reducible, inline]

abbrev Undecidability.MillerTancer.ZMul : Type

The infinite cyclic group, written multiplicatively.

Equations

• Undecidability.MillerTancer.ZMul = Multiplicative ℤ

@[reducible, inline]

abbrev Undecidability.MillerTancer.CyclicFamily (d : ℕ) : Fin d → Type

An indexed family of infinite cyclic groups.

Equations

• Undecidability.MillerTancer.CyclicFamily d x✝ = Undecidability.MillerTancer.ZMul

@[reducible, inline]

abbrev Undecidability.MillerTancer.CyclicCoprod (d : ℕ) : Type

The free product of the indicated number of infinite cyclic groups.

Equations

• Undecidability.MillerTancer.CyclicCoprod d = Monoid.CoprodI (Undecidability.MillerTancer.CyclicFamily d)

@[reducible, inline]

abbrev Undecidability.MillerTancer.RightNormalForm.R : Type

The indexed free product realizing the right-hand free group.

Equations

• Undecidability.MillerTancer.RightNormalForm.R = Undecidability.MillerTancer.CyclicCoprod 2

def Undecidability.MillerTancer.RightNormalForm.b : R

The generator b in Miller–Tancer’s right normal form construction.

Equations

• Undecidability.MillerTancer.RightNormalForm.b = Monoid.CoprodI.of (Multiplicative.ofAdd 1)

def Undecidability.MillerTancer.RightNormalForm.g : R

The generator of the second cyclic factor, representing gamma.

Equations

• Undecidability.MillerTancer.RightNormalForm.g = Monoid.CoprodI.of (Multiplicative.ofAdd 1)

def Undecidability.MillerTancer.RightNormalForm.elt : Fin 5 → R

The five right-hand basis elements in the cyclic-factor normal-form model.

Equations

• One or more equations did not get rendered due to their size.
• Undecidability.MillerTancer.RightNormalForm.elt 0 = Undecidability.MillerTancer.RightNormalForm.b

def Undecidability.MillerTancer.RightNormalForm.side : Fin 5 → Fin 2

The cyclic factor containing the two endpoints of each basis-power block.

Equations

• Undecidability.MillerTancer.RightNormalForm.side 0 = 0
• Undecidability.MillerTancer.RightNormalForm.side x✝ = 1

def Undecidability.MillerTancer.RightNormalForm.app {i j k l : Fin 2} (u : Monoid.CoprodI.NeWord (CyclicFamily 2) i j) (h : j ≠ k) (v : Monoid.CoprodI.NeWord (CyclicFamily 2) k l) : Monoid.CoprodI.NeWord (CyclicFamily 2) i l

Concatenate nonempty reduced words whose adjacent factor labels differ.

Equations

• Undecidability.MillerTancer.RightNormalForm.app u h v = u.append h v

def Undecidability.MillerTancer.RightNormalForm.block₀ (k : ℤ) (hk : k ≠ 0) : Monoid.CoprodI.NeWord (CyclicFamily 2) 0 0

The singleton reduced block representing a nonzero power of the first basis element.

Equations

• Undecidability.MillerTancer.RightNormalForm.block₀ k hk = Monoid.CoprodI.NeWord.singletonZ 0 k hk

def Undecidability.MillerTancer.RightNormalForm.blockTwisted (r : ℕ) (hr : 0 < r) (k : ℤ) (hk : k ≠ 0) : Monoid.CoprodI.NeWord (CyclicFamily 2) 1 1

The reduced block for a power of a conjugated twisted basis element.

Equations

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

def Undecidability.MillerTancer.RightNormalForm.block₁ (k : ℤ) (hk : k ≠ 0) : Monoid.CoprodI.NeWord (CyclicFamily 2) 1 1

The reduced block for a nonzero power of the second basis element.

Equations

• Undecidability.MillerTancer.RightNormalForm.block₁ k hk = Undecidability.MillerTancer.RightNormalForm.blockTwisted 1 Undecidability.MillerTancer.RightNormalForm.block₁._proof_2 k hk

def Undecidability.MillerTancer.RightNormalForm.block₂ (k : ℤ) (hk : k ≠ 0) : Monoid.CoprodI.NeWord (CyclicFamily 2) 1 1

The reduced block for a nonzero power of the third basis element.

Equations

• Undecidability.MillerTancer.RightNormalForm.block₂ k hk = Undecidability.MillerTancer.RightNormalForm.blockTwisted 2 Undecidability.MillerTancer.RightNormalForm.block₂._proof_2 k hk

def Undecidability.MillerTancer.RightNormalForm.blockConjugate (r : ℕ) (hr : 0 < r) (k : ℤ) (hk : k ≠ 0) : Monoid.CoprodI.NeWord (CyclicFamily 2) 1 1

The reduced block for a conjugate of a nonzero cyclic power.

Equations

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

def Undecidability.MillerTancer.RightNormalForm.block₃ (k : ℤ) (hk : k ≠ 0) : Monoid.CoprodI.NeWord (CyclicFamily 2) 1 1

The reduced block for a nonzero power of the fourth basis element.

Equations

• Undecidability.MillerTancer.RightNormalForm.block₃ k hk = Undecidability.MillerTancer.RightNormalForm.blockConjugate 3 Undecidability.MillerTancer.RightNormalForm.block₃._proof_2 k hk

def Undecidability.MillerTancer.RightNormalForm.block₄ (k : ℤ) (hk : k ≠ 0) : Monoid.CoprodI.NeWord (CyclicFamily 2) 1 1

The reduced block for a nonzero power of the fifth basis element.

Equations

• Undecidability.MillerTancer.RightNormalForm.block₄ k hk = Undecidability.MillerTancer.RightNormalForm.blockConjugate 4 Undecidability.MillerTancer.RightNormalForm.block₄._proof_2 k hk

def Undecidability.MillerTancer.RightNormalForm.block (i : Fin 5) (k : ℤ) (hk : k ≠ 0) : Monoid.CoprodI.NeWord (CyclicFamily 2) (side i) (side i)

The reduced block associated with a basis element and a nonzero exponent.

Equations

• Undecidability.MillerTancer.RightNormalForm.block 0 x✝¹ x✝ = Undecidability.MillerTancer.RightNormalForm.block₀ x✝¹ x✝
• Undecidability.MillerTancer.RightNormalForm.block 1 x✝¹ x✝ = Undecidability.MillerTancer.RightNormalForm.block₁ x✝¹ x✝
• Undecidability.MillerTancer.RightNormalForm.block 2 x✝¹ x✝ = Undecidability.MillerTancer.RightNormalForm.block₂ x✝¹ x✝
• Undecidability.MillerTancer.RightNormalForm.block 3 x✝¹ x✝ = Undecidability.MillerTancer.RightNormalForm.block₃ x✝¹ x✝
• Undecidability.MillerTancer.RightNormalForm.block 4 x✝¹ x✝ = Undecidability.MillerTancer.RightNormalForm.block₄ x✝¹ x✝

@[simp]

theorem Undecidability.MillerTancer.RightNormalForm.block_prod (i : Fin 5) (k : ℤ) (hk : k ≠ 0) : (block i k hk).prod = elt i ^ k

def Undecidability.MillerTancer.RightNormalForm.headValue : Fin 5 → ZMul → ZMul

The value prescribed for the first letter of a basis-power block.

Equations

• Undecidability.MillerTancer.RightNormalForm.headValue 0 x✝ = x✝
• Undecidability.MillerTancer.RightNormalForm.headValue 1 x✝ = Multiplicative.ofAdd (-1)
• Undecidability.MillerTancer.RightNormalForm.headValue 2 x✝ = Multiplicative.ofAdd (-2)
• Undecidability.MillerTancer.RightNormalForm.headValue 3 x✝ = Multiplicative.ofAdd (-3)
• Undecidability.MillerTancer.RightNormalForm.headValue 4 x✝ = Multiplicative.ofAdd (-4)

def Undecidability.MillerTancer.RightNormalForm.lastValue : Fin 5 → ZMul → ZMul

The value prescribed for the last letter of a basis-power block.

Equations

• Undecidability.MillerTancer.RightNormalForm.lastValue 0 x✝ = x✝
• Undecidability.MillerTancer.RightNormalForm.lastValue 1 x✝ = Multiplicative.ofAdd 1
• Undecidability.MillerTancer.RightNormalForm.lastValue 2 x✝ = Multiplicative.ofAdd 2
• Undecidability.MillerTancer.RightNormalForm.lastValue 3 x✝ = Multiplicative.ofAdd 3
• Undecidability.MillerTancer.RightNormalForm.lastValue 4 x✝ = Multiplicative.ofAdd 4

@[simp]

theorem Undecidability.MillerTancer.RightNormalForm.block_head (i : Fin 5) (k : ℤ) (hk : k ≠ 0) : (block i k hk).head = headValue i (Multiplicative.ofAdd k)

@[simp]

theorem Undecidability.MillerTancer.RightNormalForm.block_last (i : Fin 5) (k : ℤ) (hk : k ≠ 0) : (block i k hk).last = lastValue i (Multiplicative.ofAdd k)

theorem Undecidability.MillerTancer.RightNormalForm.side_eq_zero_iff (i : Fin 5) : side i = 0 ↔ i = 0

theorem Undecidability.MillerTancer.RightNormalForm.block_append_or_zero (i : Fin 5) (k : ℤ) (hk : k ≠ 0) : i = 0 ∨ (block i k hk).IsAppend

theorem Undecidability.MillerTancer.RightNormalForm.boundary_ne_one (i j : Fin 5) (hij : i ≠ j) (hside : side i = side j) (x y : ZMul) : lastValue i x * headValue j y ≠ 1

def Undecidability.MillerTancer.RightNormalForm.cyclicMap (i : Fin 5) : ZMul →* R

The homomorphism sending an integer exponent to a power of the corresponding basis element.

Equations

• Undecidability.MillerTancer.RightNormalForm.cyclicMap i = (zpowersHom Undecidability.MillerTancer.RightNormalForm.R) (Undecidability.MillerTancer.RightNormalForm.elt i)

def Undecidability.MillerTancer.RightNormalForm.lift : CyclicCoprod 5 →* R

The homomorphism induced by the five cyclic basis power maps.

Equations

• Undecidability.MillerTancer.RightNormalForm.lift = Monoid.CoprodI.lift Undecidability.MillerTancer.RightNormalForm.cyclicMap

structure Undecidability.MillerTancer.RightNormalForm.Image {i j : Fin 5} (w : Monoid.CoprodI.NeWord (CyclicFamily 5) i j) : Type

A reduced representative of a mapped word, together with its evaluation and boundary properties.

• word : Monoid.CoprodI.NeWord (CyclicFamily 2) (side i) (side j)

  The reduced-word representative carrying the stated evaluation and boundary properties.

• head_eq : self.word.head = headValue i w.head
• last_eq : self.word.last = lastValue j w.last
• prod_eq : self.word.prod = lift w.prod
• append_or_zero : i = 0 ∧ j = 0 ∨ self.word.IsAppend

noncomputable def Undecidability.MillerTancer.RightNormalForm.image {i j : Fin 5} (w : Monoid.CoprodI.NeWord (CyclicFamily 5) i j) : Image w

Construct the reduced image of an arbitrary source normal-form word.

Equations

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

theorem Undecidability.MillerTancer.RightNormalForm.lift_injective : Function.Injective ⇑lift

def Undecidability.MillerTancer.RightNormalForm.freeMap : FreeGroup (Fin 5) →* R

The homomorphism freely extending the displayed group-valued basis.

Equations

• Undecidability.MillerTancer.RightNormalForm.freeMap = FreeGroup.lift Undecidability.MillerTancer.RightNormalForm.elt

theorem Undecidability.MillerTancer.RightNormalForm.freeMap_eq : freeMap = lift.comp (Monoid.CoprodI.intOfFree (Fin 5))

theorem Undecidability.MillerTancer.RightNormalForm.freeMap_injective : Function.Injective ⇑freeMap

theorem Undecidability.MillerTancer.RightNormalForm.original_rightBasisMap_comp : (Monoid.CoprodI.intOfFree (Fin 2)).comp rightBasisMap = freeMap

theorem Undecidability.MillerTancer.RightNormalForm.original_rightBasisMap_injective : Function.Injective ⇑rightBasisMap