The left separated-conjugates map is injective when w ≠ 1.

def Undecidability.MillerTancer.LeftInjective.q {G : Type} [Group G] (z : G) : LeftNormalForm.LeftProduct G

The element obtained by multiplying the original normal generator by beta.

Equations

• Undecidability.MillerTancer.LeftInjective.q z = Undecidability.MillerTancer.LeftNormalForm.old z * Undecidability.MillerTancer.LeftNormalForm.beta

theorem Undecidability.MillerTancer.LeftInjective.q_ne_one {G : Type} [Group G] (z : G) : q z ≠ 1

def Undecidability.MillerTancer.LeftInjective.posRest {G : Type} [Group G] (z : G) (n : ℕ) : Monoid.CoprodI.NeWord (LeftNormalForm.OuterFactor G) LeftNormalForm.OuterIndex.base LeftNormalForm.OuterIndex.alpha

The repeated suffix of a positive-power normal-form block.

Equations

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

def Undecidability.MillerTancer.LeftInjective.posBlock {G : Type} [Group G] (z : G) (n : ℕ) : Monoid.CoprodI.NeWord (LeftNormalForm.OuterFactor G) LeftNormalForm.OuterIndex.alpha LeftNormalForm.OuterIndex.alpha

The full reduced normal-form block for a positive power.

Equations

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

def Undecidability.MillerTancer.LeftInjective.negRest {G : Type} [Group G] (z : G) (n : ℕ) : Monoid.CoprodI.NeWord (LeftNormalForm.OuterFactor G) LeftNormalForm.OuterIndex.base LeftNormalForm.OuterIndex.base

The repeated suffix of a negative-power normal-form block.

Equations

• One or more equations did not get rendered due to their size.
• Undecidability.MillerTancer.LeftInjective.negRest z 0 = Undecidability.MillerTancer.LeftNormalForm.baseSingleton (Undecidability.MillerTancer.LeftInjective.q z)⁻¹ ⋯

def Undecidability.MillerTancer.LeftInjective.negInit {G : Type} [Group G] (z : G) (n : ℕ) : Monoid.CoprodI.NeWord (LeftNormalForm.OuterFactor G) LeftNormalForm.OuterIndex.alpha LeftNormalForm.OuterIndex.base

The initial segment of a negative-power normal-form block.

Equations

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

def Undecidability.MillerTancer.LeftInjective.negBlock {G : Type} [Group G] (z : G) (n : ℕ) : Monoid.CoprodI.NeWord (LeftNormalForm.OuterFactor G) LeftNormalForm.OuterIndex.alpha LeftNormalForm.OuterIndex.alpha

The full reduced normal-form block for a negative power.

Equations

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

def Undecidability.MillerTancer.LeftInjective.leftPowerWord4 {G : Type} [Group G] (z : G) (k : ℤ) (hk : k ≠ 0) : Monoid.CoprodI.NeWord (LeftNormalForm.OuterFactor G) LeftNormalForm.OuterIndex.alpha LeftNormalForm.OuterIndex.alpha

The reduced word representing a nonzero power of the fourth left basis element.

Equations

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

theorem Undecidability.MillerTancer.LeftInjective.leftPowerWord4_ofNat {G : Type} [Group G] (z : G) (n : ℕ) : leftPowerWord4 z (Int.ofNat (n + 1)) ⋯ = posBlock z n

@[simp]

theorem Undecidability.MillerTancer.LeftInjective.leftPowerWord4_negSucc {G : Type} [Group G] (z : G) (n : ℕ) : leftPowerWord4 z (Int.negSucc n) ⋯ = negBlock z n

theorem Undecidability.MillerTancer.LeftInjective.leftPowerWord4_prod {G : Type} [Group G] (w z : G) (k : ℤ) (hk : k ≠ 0) : (leftPowerWord4 z k hk).prod = LeftNormalForm.outerLeftBasis w z 4 ^ k

def Undecidability.MillerTancer.LeftInjective.alphaVal (k : ℤ) : FreeGroup Unit

The indicated integer power of the generator of the alpha cyclic factor.

Equations

• Undecidability.MillerTancer.LeftInjective.alphaVal k = FreeGroup.of () ^ k

theorem Undecidability.MillerTancer.LeftInjective.posRest_last {G : Type} [Group G] (z : G) (n : ℕ) : (posRest z n).last = alphaVal 4

The delicate part lives on generators 1,2,3,4. Generator 0 is split off later as a separate cyclic free factor.

inductive Undecidability.MillerTancer.LeftInjective.SmallIndex : Type

The indices of the four nontrivial left basis blocks.

• one : SmallIndex
• two : SmallIndex
• three : SmallIndex
• four : SmallIndex

@[instance_reducible]

instance Undecidability.MillerTancer.LeftInjective.instDecidableEqSmallIndex : DecidableEq SmallIndex

Equations

• Undecidability.MillerTancer.LeftInjective.instDecidableEqSmallIndex x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Undecidability.MillerTancer.LeftInjective.smallBasis {G : Type} [Group G] (w z : G) : SmallIndex → LeftNormalForm.MillerLeft G

The four nontrivial basis elements used in the left injectivity argument.

Equations

• Undecidability.MillerTancer.LeftInjective.smallBasis w z Undecidability.MillerTancer.LeftInjective.SmallIndex.one = Undecidability.MillerTancer.LeftNormalForm.outerLeftBasis w z 1
• Undecidability.MillerTancer.LeftInjective.smallBasis w z Undecidability.MillerTancer.LeftInjective.SmallIndex.two = Undecidability.MillerTancer.LeftNormalForm.outerLeftBasis w z 2
• Undecidability.MillerTancer.LeftInjective.smallBasis w z Undecidability.MillerTancer.LeftInjective.SmallIndex.three = Undecidability.MillerTancer.LeftNormalForm.outerLeftBasis w z 3
• Undecidability.MillerTancer.LeftInjective.smallBasis w z Undecidability.MillerTancer.LeftInjective.SmallIndex.four = Undecidability.MillerTancer.LeftNormalForm.outerLeftBasis w z 4

def Undecidability.MillerTancer.LeftInjective.smallWord {G : Type} [Group G] (w z : G) (hw : w ≠ 1) (i : SmallIndex) (k : ℤ) (hk : k ≠ 0) : Monoid.CoprodI.NeWord (LeftNormalForm.OuterFactor G) LeftNormalForm.OuterIndex.alpha LeftNormalForm.OuterIndex.alpha

The reduced word realizing a nonzero power of a nontrivial left basis element.

Equations

• Undecidability.MillerTancer.LeftInjective.smallWord w z hw Undecidability.MillerTancer.LeftInjective.SmallIndex.one k hk = Undecidability.MillerTancer.LeftNormalForm.leftPowerWord1 k hk
• Undecidability.MillerTancer.LeftInjective.smallWord w z hw Undecidability.MillerTancer.LeftInjective.SmallIndex.two k hk = Undecidability.MillerTancer.LeftNormalForm.leftPowerWord2 k hk
• Undecidability.MillerTancer.LeftInjective.smallWord w z hw Undecidability.MillerTancer.LeftInjective.SmallIndex.three k hk = Undecidability.MillerTancer.LeftNormalForm.leftPowerWord3 w hw k hk
• Undecidability.MillerTancer.LeftInjective.smallWord w z hw Undecidability.MillerTancer.LeftInjective.SmallIndex.four k hk = Undecidability.MillerTancer.LeftInjective.leftPowerWord4 z k hk

@[simp]

theorem Undecidability.MillerTancer.LeftInjective.smallWord_prod {G : Type} [Group G] (w z : G) (hw : w ≠ 1) (i : SmallIndex) (k : ℤ) (hk : k ≠ 0) : (smallWord w z hw i k hk).prod = smallBasis w z i ^ k

def Undecidability.MillerTancer.LeftInjective.smallHeadExp : SmallIndex → ℤ → ℤ

The initial cyclic exponent of a nontrivial left basis block.

Equations

• Undecidability.MillerTancer.LeftInjective.smallHeadExp Undecidability.MillerTancer.LeftInjective.SmallIndex.one x✝ = -1
• Undecidability.MillerTancer.LeftInjective.smallHeadExp Undecidability.MillerTancer.LeftInjective.SmallIndex.two x✝ = -2
• Undecidability.MillerTancer.LeftInjective.smallHeadExp Undecidability.MillerTancer.LeftInjective.SmallIndex.three x✝ = -3
• Undecidability.MillerTancer.LeftInjective.smallHeadExp Undecidability.MillerTancer.LeftInjective.SmallIndex.four x✝ = if 0 < x✝ then -2 else -4

def Undecidability.MillerTancer.LeftInjective.smallLastExp : SmallIndex → ℤ → ℤ

The final cyclic exponent of a nontrivial left basis block.

Equations

• Undecidability.MillerTancer.LeftInjective.smallLastExp Undecidability.MillerTancer.LeftInjective.SmallIndex.one x✝ = 1
• Undecidability.MillerTancer.LeftInjective.smallLastExp Undecidability.MillerTancer.LeftInjective.SmallIndex.two x✝ = 2
• Undecidability.MillerTancer.LeftInjective.smallLastExp Undecidability.MillerTancer.LeftInjective.SmallIndex.three x✝ = 3
• Undecidability.MillerTancer.LeftInjective.smallLastExp Undecidability.MillerTancer.LeftInjective.SmallIndex.four x✝ = if 0 < x✝ then 4 else 2

theorem Undecidability.MillerTancer.LeftInjective.smallWord_head {G : Type} [Group G] (w z : G) (hw : w ≠ 1) (i : SmallIndex) (k : ℤ) (hk : k ≠ 0) : (smallWord w z hw i k hk).head = alphaVal (smallHeadExp i k)

theorem Undecidability.MillerTancer.LeftInjective.smallWord_last {G : Type} [Group G] (w z : G) (hw : w ≠ 1) (i : SmallIndex) (k : ℤ) (hk : k ≠ 0) : (smallWord w z hw i k hk).last = alphaVal (smallLastExp i k)

def Undecidability.MillerTancer.LeftInjective.tailTwo {G : Type} [Group G] (k : ℤ) (hk : k ≠ 0) : Monoid.CoprodI.NeWord (LeftNormalForm.OuterFactor G) LeftNormalForm.OuterIndex.base LeftNormalForm.OuterIndex.alpha

The reduced tail exposing the base letter in a power of the second left basis element.

Equations

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

structure Undecidability.MillerTancer.LeftInjective.Prefix {G : Type} [Group G] (word : Monoid.CoprodI.NeWord (LeftNormalForm.OuterFactor G) LeftNormalForm.OuterIndex.alpha LeftNormalForm.OuterIndex.alpha) (x : LeftNormalForm.LeftProduct G) : Type

A reduced prefix decomposition exposing a prescribed base-group letter.

• tail : Monoid.CoprodI.NeWord (LeftNormalForm.OuterFactor G) LeftNormalForm.OuterIndex.base LeftNormalForm.OuterIndex.alpha

  The reduced tail beginning with the prescribed base-group letter.

• tail_head : self.tail.head = x
• prod_eq : word.prod = LeftNormalForm.outerAlpha ^ (-2) * self.tail.prod

def Undecidability.MillerTancer.LeftInjective.prefixTwo {G : Type} [Group G] (k : ℤ) (hk : k ≠ 0) : Prefix (LeftNormalForm.leftPowerWord2 k hk) LeftNormalForm.beta⁻¹

The prefix decomposition of a nonzero power of the second left basis element.

Equations

• Undecidability.MillerTancer.LeftInjective.prefixTwo k hk = { tail := Undecidability.MillerTancer.LeftInjective.tailTwo k hk, tail_head := ⋯, prod_eq := ⋯ }

def Undecidability.MillerTancer.LeftInjective.prefixFourPos {G : Type} [Group G] (z : G) (n : ℕ) : Prefix (posBlock z n) (q z)

The prefix decomposition of a positive power of the fourth left basis element.

Equations

• Undecidability.MillerTancer.LeftInjective.prefixFourPos z n = { tail := Undecidability.MillerTancer.LeftInjective.posRest z n, tail_head := ⋯, prod_eq := ⋯ }

theorem Undecidability.MillerTancer.LeftInjective.tailTwo_last {G : Type} [Group G] (k : ℤ) (hk : k ≠ 0) : (tailTwo k hk).last = alphaVal 2

@[reducible, inline]

abbrev Undecidability.MillerTancer.LeftInjective.IsAppend {G : Type} [Group G] {i j : LeftNormalForm.OuterIndex} (w : Monoid.CoprodI.NeWord (LeftNormalForm.OuterFactor G) i j) : Prop

A reduced word has an append constructor rather than a singleton constructor.

Equations

• Undecidability.MillerTancer.LeftInjective.IsAppend w = w.IsAppend

theorem Undecidability.MillerTancer.LeftInjective.tailTwo_isAppend {G : Type} [Group G] (k : ℤ) (hk : k ≠ 0) : IsAppend (tailTwo k hk)

theorem Undecidability.MillerTancer.LeftInjective.posRest_isAppend {G : Type} [Group G] (z : G) (n : ℕ) : IsAppend (posRest z n)

theorem Undecidability.MillerTancer.LeftInjective.merge_head_of_isAppend_left {G : Type} [Group G] {i j k : LeftNormalForm.OuterIndex} (u : Monoid.CoprodI.NeWord (LeftNormalForm.OuterFactor G) i j) (v : Monoid.CoprodI.NeWord (LeftNormalForm.OuterFactor G) j k) (h : u.last * v.head ≠ 1) (hu : IsAppend u) : (u.merge v h).head = u.head

theorem Undecidability.MillerTancer.LeftInjective.smallWord_isAppend {G : Type} [Group G] (w z : G) (hw : w ≠ 1) (i : SmallIndex) (k : ℤ) (hk : k ≠ 0) : IsAppend (smallWord w z hw i k hk)

def Undecidability.MillerTancer.LeftInjective.Exceptional (i : SmallIndex) (r : ℤ) (j : SmallIndex) (s : ℤ) : Prop

The two signed boundary configurations requiring a separate cancellation argument.

Equations

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

theorem Undecidability.MillerTancer.LeftInjective.boundary_ne_one {G : Type} [Group G] (w z : G) (hw : w ≠ 1) (i j : SmallIndex) (r s : ℤ) (hr : r ≠ 0) (hs : s ≠ 0) (hij : i ≠ j) (hex : ¬Exceptional i r j s) (v : Monoid.CoprodI.NeWord (LeftNormalForm.OuterFactor G) LeftNormalForm.OuterIndex.alpha LeftNormalForm.OuterIndex.alpha) (hv : v.head = alphaVal (smallHeadExp j s)) : (smallWord w z hw i r hr).last * v.head ≠ 1

def Undecidability.MillerTancer.LeftInjective.evalSmall {G : Type} [Group G] (w z : G) : List (SmallIndex × ℤ) → LeftNormalForm.MillerLeft G

The product of the indicated powers of the four nontrivial left basis elements.

Equations

• Undecidability.MillerTancer.LeftInjective.evalSmall w z [] = 1
• Undecidability.MillerTancer.LeftInjective.evalSmall w z (p :: l) = Undecidability.MillerTancer.LeftInjective.smallBasis w z p.1 ^ p.2 * Undecidability.MillerTancer.LeftInjective.evalSmall w z l

structure Undecidability.MillerTancer.LeftInjective.Image {G : Type} [Group G] (w z : G) (hw : w ≠ 1) (p : SmallIndex × ℤ) (rest : List (SmallIndex × ℤ)) : Type

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

• word : Monoid.CoprodI.NeWord (LeftNormalForm.OuterFactor G) LeftNormalForm.OuterIndex.alpha LeftNormalForm.OuterIndex.alpha

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

• prod_eq : self.word.prod = evalSmall w z (p :: rest)
• head_eq : self.word.head = alphaVal (smallHeadExp p.1 p.2)
• prefixTwo : p.1 = SmallIndex.two → Prefix self.word LeftNormalForm.beta⁻¹

  The prefix decomposition when the leading basis index is the second one.

• prefixFourPositive : p.1 = SmallIndex.four → 0 < p.2 → Prefix self.word (q z)

  The prefix decomposition for a positive leading power of the fourth basis element.

def Undecidability.MillerTancer.LeftInjective.singletonImage {G : Type} [Group G] (w z : G) (hw : w ≠ 1) (i : SmallIndex) (k : ℤ) (hk : k ≠ 0) : Image w z hw (i, k) []

The reduced image of a one-block input word.

Equations

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

noncomputable def Undecidability.MillerTancer.LeftInjective.mergedImage {G : Type} [Group G] (w z : G) (hw : w ≠ 1) (i j : SmallIndex) (r s : ℤ) (hr : r ≠ 0) (hs : s ≠ 0) (rest : List (SmallIndex × ℤ)) (tail : Image w z hw (j, s) rest) (hij : i ≠ j) (hex : ¬Exceptional i r j s) : Image w z hw (i, r) ((j, s) :: rest)

The reduced image formed when two adjacent input blocks are merged.

Equations

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

def Undecidability.MillerTancer.LeftInjective.special24Tail {G : Type} [Group G] (z : G) (r : ℤ) (hr : r ≠ 0) (v : Monoid.CoprodI.NeWord (LeftNormalForm.OuterFactor G) LeftNormalForm.OuterIndex.base LeftNormalForm.OuterIndex.alpha) (hv : v.head = q z) : Monoid.CoprodI.NeWord (LeftNormalForm.OuterFactor G) LeftNormalForm.OuterIndex.base LeftNormalForm.OuterIndex.alpha

The reduced tail for the exceptional second-to-fourth block boundary.

Equations

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

def Undecidability.MillerTancer.LeftInjective.special24Word {G : Type} [Group G] (z : G) (r : ℤ) (hr : r ≠ 0) (v : Monoid.CoprodI.NeWord (LeftNormalForm.OuterFactor G) LeftNormalForm.OuterIndex.base LeftNormalForm.OuterIndex.alpha) (hv : v.head = q z) : Monoid.CoprodI.NeWord (LeftNormalForm.OuterFactor G) LeftNormalForm.OuterIndex.alpha LeftNormalForm.OuterIndex.alpha

The reduced word for the exceptional second-to-fourth block boundary.

Equations

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

theorem Undecidability.MillerTancer.LeftInjective.special24Word_prod {G : Type} [Group G] (z : G) (r : ℤ) (hr : r ≠ 0) (right : Monoid.CoprodI.NeWord (LeftNormalForm.OuterFactor G) LeftNormalForm.OuterIndex.alpha LeftNormalForm.OuterIndex.alpha) (pf : Prefix right (q z)) : (special24Word z r hr pf.tail ⋯).prod = (LeftNormalForm.leftPowerWord2 r hr).prod * right.prod

def Undecidability.MillerTancer.LeftInjective.special24Image {G : Type} [Group G] (w z : G) (hw : w ≠ 1) (r s : ℤ) (hr : r ≠ 0) (hpos : 0 < s) (rest : List (SmallIndex × ℤ)) (tail : Image w z hw (SmallIndex.four, s) rest) : Image w z hw (SmallIndex.two, r) ((SmallIndex.four, s) :: rest)

The image construction for an exceptional second-to-fourth block boundary.

Equations

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

theorem Undecidability.MillerTancer.LeftInjective.negInit_isAppend {G : Type} [Group G] (z : G) (n : ℕ) : IsAppend (negInit z n)

theorem Undecidability.MillerTancer.LeftInjective.negInit_head {G : Type} [Group G] (z : G) (n : ℕ) : (negInit z n).head = alphaVal (-4)

theorem Undecidability.MillerTancer.LeftInjective.negInit_last {G : Type} [Group G] (z : G) (n : ℕ) : (negInit z n).last = (q z)⁻¹

noncomputable def Undecidability.MillerTancer.LeftInjective.special42Image {G : Type} [Group G] (w z : G) (hw : w ≠ 1) (n : ℕ) (s : ℤ) (rest : List (SmallIndex × ℤ)) (tail : Image w z hw (SmallIndex.two, s) rest) : Image w z hw (SmallIndex.four, Int.negSucc n) ((SmallIndex.two, s) :: rest)

The image construction for an exceptional fourth-to-second block boundary.

Equations

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

noncomputable def Undecidability.MillerTancer.LeftInjective.imageList {G : Type} [Group G] (w z : G) (hw : w ≠ 1) (p : SmallIndex × ℤ) (rest : List (SmallIndex × ℤ)) (hp : p.2 ≠ 0) (hrest : ∀ q ∈ rest, q.2 ≠ 0) (hchain : List.IsChain (fun (a b : SmallIndex × ℤ) => a.1 ≠ b.1) (p :: rest)) : Image w z hw p rest

The reduced image of a list of nontrivial left basis powers.

Equations

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

@[reducible, inline]

abbrev Undecidability.MillerTancer.LeftInjective.SmallCyclic : SmallIndex → Type

The infinite cyclic free group assigned to each of the four basis indices.

Equations

• Undecidability.MillerTancer.LeftInjective.SmallCyclic x✝ = FreeGroup Unit

theorem Undecidability.MillerTancer.LeftInjective.exists_small_image {G : Type} [Group G] (w z : G) (hw : w ≠ 1) (x : FreeGroup SmallIndex) (hx : x ≠ 1) : ∃ (u : Monoid.CoprodI.NeWord (LeftNormalForm.OuterFactor G) LeftNormalForm.OuterIndex.alpha LeftNormalForm.OuterIndex.alpha), u.prod = (FreeGroup.lift (smallBasis w z)) x

def Undecidability.MillerTancer.LeftInjective.smallOfFin : Fin 4 → SmallIndex

Convert a four-element finite index to the named basis index.

Equations

• Undecidability.MillerTancer.LeftInjective.smallOfFin 0 = Undecidability.MillerTancer.LeftInjective.SmallIndex.one
• Undecidability.MillerTancer.LeftInjective.smallOfFin 1 = Undecidability.MillerTancer.LeftInjective.SmallIndex.two
• Undecidability.MillerTancer.LeftInjective.smallOfFin 2 = Undecidability.MillerTancer.LeftInjective.SmallIndex.three
• Undecidability.MillerTancer.LeftInjective.smallOfFin 3 = Undecidability.MillerTancer.LeftInjective.SmallIndex.four

def Undecidability.MillerTancer.LeftInjective.finOfSmall : SmallIndex → Fin 4

Convert a named basis index to its four-element finite index.

Equations

• Undecidability.MillerTancer.LeftInjective.finOfSmall Undecidability.MillerTancer.LeftInjective.SmallIndex.one = 0
• Undecidability.MillerTancer.LeftInjective.finOfSmall Undecidability.MillerTancer.LeftInjective.SmallIndex.two = 1
• Undecidability.MillerTancer.LeftInjective.finOfSmall Undecidability.MillerTancer.LeftInjective.SmallIndex.three = 2
• Undecidability.MillerTancer.LeftInjective.finOfSmall Undecidability.MillerTancer.LeftInjective.SmallIndex.four = 3

def Undecidability.MillerTancer.LeftInjective.toSmall : FreeGroup (Fin 4) →* FreeGroup SmallIndex

The free-group homomorphism renaming the four finite indices to named basis indices.

Equations

• Undecidability.MillerTancer.LeftInjective.toSmall = FreeGroup.lift fun (i : Fin 4) => FreeGroup.of (Undecidability.MillerTancer.LeftInjective.smallOfFin i)

def Undecidability.MillerTancer.LeftInjective.fromSmall : FreeGroup SmallIndex →* FreeGroup (Fin 4)

The inverse free-group homomorphism renaming the named indices to finite indices.

Equations

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

theorem Undecidability.MillerTancer.LeftInjective.toSmall_injective : Function.Injective ⇑toSmall

theorem Undecidability.MillerTancer.LeftInjective.smallLift_comp_toSmall {G : Type} [Group G] (w z : G) : (FreeGroup.lift (smallBasis w z)).comp toSmall = LeftSplit.tailMap w z

theorem Undecidability.MillerTancer.LeftInjective.exists_fin_tail_image {G : Type} [Group G] (w z : G) (hw : w ≠ 1) (x : FreeGroup (Fin 4)) (hx : x ≠ 1) : ∃ (u : Monoid.CoprodI.NeWord (LeftNormalForm.OuterFactor G) LeftNormalForm.OuterIndex.alpha LeftNormalForm.OuterIndex.alpha), u.prod = (LeftSplit.tailMap w z) x

noncomputable def Undecidability.MillerTancer.LeftInjective.tailImageFin {G : Type} [Group G] (w z : G) (hw : w ≠ 1) (x : FreeGroup (Fin 4)) (hx : x ≠ 1) : Monoid.CoprodI.NeWord (LeftNormalForm.OuterFactor G) LeftNormalForm.OuterIndex.alpha LeftNormalForm.OuterIndex.alpha

A reduced representative of the image of a nonidentity four-generator free word.

Equations

• Undecidability.MillerTancer.LeftInjective.tailImageFin w z hw x hx = Classical.choose ⋯

theorem Undecidability.MillerTancer.LeftInjective.tailImageFin_prod {G : Type} [Group G] (w z : G) (hw : w ≠ 1) (x : FreeGroup (Fin 4)) (hx : x ≠ 1) : (tailImageFin w z hw x hx).prod = (LeftSplit.tailMap w z) x

theorem Undecidability.MillerTancer.LeftInjective.outerLeftBasis_lift_injective {G : Type} [Group G] (w z : G) (hw : w ≠ 1) : Function.Injective ⇑(FreeGroup.lift (LeftNormalForm.outerLeftBasis w z))

The complete left free-basis lemma used in the amalgamated-product proof.