The left free-basis calculation in Gordon's Lemma 2.1.

We split G * F(a, alpha) into the free product of G, <a>, and <alpha>. The exponent assignment is kept abstract: positivity makes each displayed block nonempty, while injectivity is exactly what rules out the only possible boundary cancellation between two old-generator blocks.

@[reducible, inline]

abbrev Undecidability.Gordon.LeftNormalForm.SplitLeft (G : Type) [Group G] : Type

The left group with its cyclic generators separated into individual free factors.

Equations

• Undecidability.Gordon.LeftNormalForm.SplitLeft G = Undecidability.MillerTancer.LeftNormalForm.LeftProduct G

def Undecidability.Gordon.LeftNormalForm.a {G : Type} [Group G] : SplitLeft G

The generator a in Gordon’s left normal form construction.

Equations

• Undecidability.Gordon.LeftNormalForm.a = Undecidability.MillerTancer.LeftNormalForm.alpha

def Undecidability.Gordon.LeftNormalForm.auxiliaryAlpha {G : Type} [Group G] : SplitLeft G

The second cyclic generator, used as the auxiliary letter alpha.

Equations

• Undecidability.Gordon.LeftNormalForm.auxiliaryAlpha = Undecidability.MillerTancer.LeftNormalForm.beta

def Undecidability.Gordon.LeftNormalForm.degreeInt {d : ℕ} (degree : Fin d → ℕ) (i : Fin d) : ℤ

The assigned natural-number exponent, regarded as an integer.

Equations

• Undecidability.Gordon.LeftNormalForm.degreeInt degree i = ↑(degree i)

def Undecidability.Gordon.LeftNormalForm.oldElement {d : ℕ} {G : Type} [Group G] (degree : Fin d → ℕ) (x : Fin d → G) (i : Fin d) : SplitLeft G

The encoded original generator between the indicated powers of the two cyclic generators.

Equations

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

def Undecidability.Gordon.LeftNormalForm.splitBasis {d : ℕ} {G : Type} [Group G] (degree : Fin d → ℕ) (x : Fin d → G) (w : G) : BasisIndex d → SplitLeft G

The proposed amalgamating basis, realized in the separated left factors.

Equations

• One or more equations did not get rendered due to their size.
• Undecidability.Gordon.LeftNormalForm.splitBasis degree x w (Undecidability.Gordon.BasisIndex.old i) = Undecidability.Gordon.LeftNormalForm.oldElement degree x i

def Undecidability.Gordon.LeftNormalForm.cyclicSingleton {G : Type} [Group G] (i : MillerTancer.LeftNormalForm.LeftIndex) (k : ℤ) (hk : k ≠ 0) (hi : i = MillerTancer.LeftNormalForm.LeftIndex.alpha ∨ i = MillerTancer.LeftNormalForm.LeftIndex.beta) : Monoid.CoprodI.NeWord (MillerTancer.LeftNormalForm.LeftFactor G) i i

The one-letter reduced word representing a nonzero power in a cyclic factor.

Equations

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

def Undecidability.Gordon.LeftNormalForm.alphaSingleton {G : Type} [Group G] (k : ℤ) (hk : k ≠ 0) : Monoid.CoprodI.NeWord (MillerTancer.LeftNormalForm.LeftFactor G) MillerTancer.LeftNormalForm.LeftIndex.alpha MillerTancer.LeftNormalForm.LeftIndex.alpha

The one-letter reduced word in the alpha factor.

Equations

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

def Undecidability.Gordon.LeftNormalForm.betaSingleton {G : Type} [Group G] (k : ℤ) (hk : k ≠ 0) : Monoid.CoprodI.NeWord (MillerTancer.LeftNormalForm.LeftFactor G) MillerTancer.LeftNormalForm.LeftIndex.beta MillerTancer.LeftNormalForm.LeftIndex.beta

The one-letter reduced word in the beta factor.

Equations

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

def Undecidability.Gordon.LeftNormalForm.oldSingleton {G : Type} [Group G] (g : G) (hg : g ≠ 1) : Monoid.CoprodI.NeWord (MillerTancer.LeftNormalForm.LeftFactor G) MillerTancer.LeftNormalForm.LeftIndex.old MillerTancer.LeftNormalForm.LeftIndex.old

The one-letter reduced word representing a nonidentity element of the original group.

Equations

• Undecidability.Gordon.LeftNormalForm.oldSingleton g hg = Monoid.CoprodI.NeWord.singleton g hg

@[simp]

theorem Undecidability.Gordon.LeftNormalForm.alphaSingleton_prod {G : Type} [Group G] (k : ℤ) (hk : k ≠ 0) : (alphaSingleton k hk).prod = a ^ k

@[simp]

theorem Undecidability.Gordon.LeftNormalForm.betaSingleton_prod {G : Type} [Group G] (k : ℤ) (hk : k ≠ 0) : (betaSingleton k hk).prod = auxiliaryAlpha ^ k

@[simp]

theorem Undecidability.Gordon.LeftNormalForm.old_one {G : Type} [Group G] : MillerTancer.LeftNormalForm.old 1 = 1

def Undecidability.Gordon.LeftNormalForm.conjugatePowerA {G : Type} [Group G] (k : ℤ) (hk : k ≠ 0) : Monoid.CoprodI.NeWord (MillerTancer.LeftNormalForm.LeftFactor G) MillerTancer.LeftNormalForm.LeftIndex.alpha MillerTancer.LeftNormalForm.LeftIndex.alpha

The reduced word representing a nonzero power of the first conjugated cyclic generator.

Equations

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

def Undecidability.Gordon.LeftNormalForm.conjugatePowerAlpha {G : Type} [Group G] (k : ℤ) (hk : k ≠ 0) : Monoid.CoprodI.NeWord (MillerTancer.LeftNormalForm.LeftFactor G) MillerTancer.LeftNormalForm.LeftIndex.beta MillerTancer.LeftNormalForm.LeftIndex.beta

The reduced word representing a nonzero power of the second conjugated cyclic generator.

Equations

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

@[simp]

theorem Undecidability.Gordon.LeftNormalForm.conjugatePowerA_prod {G : Type} [Group G] (k : ℤ) (hk : k ≠ 0) : (conjugatePowerA k hk).prod = (a * auxiliaryAlpha * a⁻¹) ^ k

@[simp]

theorem Undecidability.Gordon.LeftNormalForm.conjugatePowerAlpha_prod {G : Type} [Group G] (k : ℤ) (hk : k ≠ 0) : (conjugatePowerAlpha k hk).prod = (auxiliaryAlpha * a * auxiliaryAlpha⁻¹) ^ k

theorem Undecidability.Gordon.LeftNormalForm.degreeInt_ne_zero {d : ℕ} (degree : Fin d → ℕ) (hdegree : ∀ (i : Fin d), 0 < degree i) (i : Fin d) : degreeInt degree i ≠ 0

noncomputable def Undecidability.Gordon.LeftNormalForm.oldBlock {d : ℕ} {G : Type} [Group G] (degree : Fin d → ℕ) (hdegree : ∀ (i : Fin d), 0 < degree i) (x : Fin d → G) (i : Fin d) : Monoid.CoprodI.NeWord (MillerTancer.LeftNormalForm.LeftFactor G) MillerTancer.LeftNormalForm.LeftIndex.alpha MillerTancer.LeftNormalForm.LeftIndex.beta

The reduced block representing a power of an encoded original generator.

Equations

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

@[simp]

theorem Undecidability.Gordon.LeftNormalForm.oldBlock_prod {d : ℕ} {G : Type} [Group G] (degree : Fin d → ℕ) (hdegree : ∀ (i : Fin d), 0 < degree i) (x : Fin d → G) (i : Fin d) : (oldBlock degree hdegree x i).prod = oldElement degree x i

@[simp]

theorem Undecidability.Gordon.LeftNormalForm.oldBlock_head {d : ℕ} {G : Type} [Group G] (degree : Fin d → ℕ) (hdegree : ∀ (i : Fin d), 0 < degree i) (x : Fin d → G) (i : Fin d) : (oldBlock degree hdegree x i).head = FreeGroup.of () ^ (-degreeInt degree i)

@[simp]

theorem Undecidability.Gordon.LeftNormalForm.oldBlock_last {d : ℕ} {G : Type} [Group G] (degree : Fin d → ℕ) (hdegree : ∀ (i : Fin d), 0 < degree i) (x : Fin d → G) (i : Fin d) : (oldBlock degree hdegree x i).last = FreeGroup.of () ^ degreeInt degree i

def Undecidability.Gordon.LeftNormalForm.commutatorBlock {G : Type} [Group G] (w : G) (hw : w ≠ 1) : Monoid.CoprodI.NeWord (MillerTancer.LeftNormalForm.LeftFactor G) MillerTancer.LeftNormalForm.LeftIndex.old MillerTancer.LeftNormalForm.LeftIndex.beta

The reduced block representing the distinguished commutator.

Equations

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

@[simp]

theorem Undecidability.Gordon.LeftNormalForm.commutatorBlock_prod {G : Type} [Group G] (w : G) (hw : w ≠ 1) : (commutatorBlock w hw).prod = MillerTancer.LeftNormalForm.old w * auxiliaryAlpha ^ 2 * (MillerTancer.LeftNormalForm.old w)⁻¹ * (auxiliaryAlpha ^ 2)⁻¹

structure Undecidability.Gordon.LeftNormalForm.PackedWord (G : Type) [Group G] : Type

A nonempty reduced word packaged with its two endpoint factor labels.

• first : MillerTancer.LeftNormalForm.LeftIndex

  The label of the factor containing the first letter.

• last : MillerTancer.LeftNormalForm.LeftIndex

  The label of the factor containing the last letter.

• word : Monoid.CoprodI.NeWord (MillerTancer.LeftNormalForm.LeftFactor G) self.first self.last

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

def Undecidability.Gordon.LeftNormalForm.PackedWord.headLetter {G : Type} [Group G] (u : PackedWord G) : (i : MillerTancer.LeftNormalForm.LeftIndex) × MillerTancer.LeftNormalForm.LeftFactor G i

The first letter, paired with its factor label.

Equations

• u.headLetter = ⟨u.first, u.word.head⟩

def Undecidability.Gordon.LeftNormalForm.PackedWord.lastLetter {G : Type} [Group G] (u : PackedWord G) : (i : MillerTancer.LeftNormalForm.LeftIndex) × MillerTancer.LeftNormalForm.LeftFactor G i

The last letter, paired with its factor label.

Equations

• u.lastLetter = ⟨u.last, u.word.last⟩

def Undecidability.Gordon.LeftNormalForm.positivePacked {G : Type} [Group G] {i j : MillerTancer.LeftNormalForm.LeftIndex} (u : Monoid.CoprodI.NeWord (MillerTancer.LeftNormalForm.LeftFactor G) i j) (hij : j ≠ i) (n : ℕ) : PackedWord G

A positive power of a cyclically reduced word, packaged with its endpoints.

Equations

• Undecidability.Gordon.LeftNormalForm.positivePacked u hij n = { first := i, last := j, word := Undecidability.MillerTancer.LeftNormalForm.positivePowerWord u hij n }

def Undecidability.Gordon.LeftNormalForm.negativePacked {G : Type} [Group G] {i j : MillerTancer.LeftNormalForm.LeftIndex} (u : Monoid.CoprodI.NeWord (MillerTancer.LeftNormalForm.LeftFactor G) i j) (hij : j ≠ i) (n : ℕ) : PackedWord G

The inverse of a positive power, with the endpoint labels exchanged.

Equations

• Undecidability.Gordon.LeftNormalForm.negativePacked u hij n = { first := j, last := i, word := (Undecidability.MillerTancer.LeftNormalForm.positivePowerWord u hij n).inv }

def Undecidability.Gordon.LeftNormalForm.cyclicPowerPacked {G : Type} [Group G] {i j : MillerTancer.LeftNormalForm.LeftIndex} (u : Monoid.CoprodI.NeWord (MillerTancer.LeftNormalForm.LeftFactor G) i j) (hij : j ≠ i) (k : ℤ) (hk : k ≠ 0) : PackedWord G

A nonzero integer power of a cyclically reduced word, with its endpoint labels.

Equations

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

@[simp]

theorem Undecidability.Gordon.LeftNormalForm.positivePowerWord_head {G : Type} [Group G] {i j : MillerTancer.LeftNormalForm.LeftIndex} (u : Monoid.CoprodI.NeWord (MillerTancer.LeftNormalForm.LeftFactor G) i j) (hij : j ≠ i) (n : ℕ) : (MillerTancer.LeftNormalForm.positivePowerWord u hij n).head = u.head

@[simp]

theorem Undecidability.Gordon.LeftNormalForm.positivePowerWord_last {G : Type} [Group G] {i j : MillerTancer.LeftNormalForm.LeftIndex} (u : Monoid.CoprodI.NeWord (MillerTancer.LeftNormalForm.LeftFactor G) i j) (hij : j ≠ i) (n : ℕ) : (MillerTancer.LeftNormalForm.positivePowerWord u hij n).last = u.last

theorem Undecidability.Gordon.LeftNormalForm.cyclicPowerPacked_prod {G : Type} [Group G] {i j : MillerTancer.LeftNormalForm.LeftIndex} (u : Monoid.CoprodI.NeWord (MillerTancer.LeftNormalForm.LeftFactor G) i j) (hij : j ≠ i) (k : ℤ) (hk : k ≠ 0) : (cyclicPowerPacked u hij k hk).word.prod = u.prod ^ k

theorem Undecidability.Gordon.LeftNormalForm.cyclicPowerPacked_head_pos {G : Type} [Group G] {i j : MillerTancer.LeftNormalForm.LeftIndex} (u : Monoid.CoprodI.NeWord (MillerTancer.LeftNormalForm.LeftFactor G) i j) (hij : j ≠ i) (k : ℤ) (hk : k ≠ 0) (hpos : 0 < k) : (cyclicPowerPacked u hij k hk).headLetter = ⟨i, u.head⟩

theorem Undecidability.Gordon.LeftNormalForm.cyclicPowerPacked_last_pos {G : Type} [Group G] {i j : MillerTancer.LeftNormalForm.LeftIndex} (u : Monoid.CoprodI.NeWord (MillerTancer.LeftNormalForm.LeftFactor G) i j) (hij : j ≠ i) (k : ℤ) (hk : k ≠ 0) (hpos : 0 < k) : (cyclicPowerPacked u hij k hk).lastLetter = ⟨j, u.last⟩

theorem Undecidability.Gordon.LeftNormalForm.cyclicPowerPacked_head_neg {G : Type} [Group G] {i j : MillerTancer.LeftNormalForm.LeftIndex} (u : Monoid.CoprodI.NeWord (MillerTancer.LeftNormalForm.LeftFactor G) i j) (hij : j ≠ i) (k : ℤ) (hk : k ≠ 0) (hneg : k < 0) : (cyclicPowerPacked u hij k hk).headLetter = ⟨j, u.last⁻¹⟩

theorem Undecidability.Gordon.LeftNormalForm.cyclicPowerPacked_last_neg {G : Type} [Group G] {i j : MillerTancer.LeftNormalForm.LeftIndex} (u : Monoid.CoprodI.NeWord (MillerTancer.LeftNormalForm.LeftFactor G) i j) (hij : j ≠ i) (k : ℤ) (hk : k ≠ 0) (hneg : k < 0) : (cyclicPowerPacked u hij k hk).lastLetter = ⟨i, u.head⁻¹⟩

noncomputable def Undecidability.Gordon.LeftNormalForm.powerPacked {d : ℕ} {G : Type} [Group G] (degree : Fin d → ℕ) (hdegree : ∀ (i : Fin d), 0 < degree i) (x : Fin d → G) (w : G) (hw : w ≠ 1) (i : BasisIndex d) (k : ℤ) (hk : k ≠ 0) : PackedWord G

The reduced block representing a nonzero power of a proposed basis element.

Equations

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

@[simp]

theorem Undecidability.Gordon.LeftNormalForm.powerPacked_old {d : ℕ} {G : Type} [Group G] (degree : Fin d → ℕ) (hdegree : ∀ (i : Fin d), 0 < degree i) (x : Fin d → G) (w : G) (hw : w ≠ 1) (i : Fin d) (k : ℤ) (hk : k ≠ 0) : powerPacked degree hdegree x w hw (BasisIndex.old i) k hk = cyclicPowerPacked (oldBlock degree hdegree x i) conjugatePowerA._proof_3 k hk

@[simp]

theorem Undecidability.Gordon.LeftNormalForm.powerPacked_commutator {d : ℕ} {G : Type} [Group G] (degree : Fin d → ℕ) (hdegree : ∀ (i : Fin d), 0 < degree i) (x : Fin d → G) (w : G) (hw : w ≠ 1) (k : ℤ) (hk : k ≠ 0) : powerPacked degree hdegree x w hw BasisIndex.commutator k hk = cyclicPowerPacked (commutatorBlock w hw) commutatorBlock._proof_2 k hk

def Undecidability.Gordon.LeftNormalForm.alphaLetter {G : Type} (k : ℤ) : (i : MillerTancer.LeftNormalForm.LeftIndex) × MillerTancer.LeftNormalForm.LeftFactor G i

An integer power in the alpha factor, paired with its factor label.

Equations

• Undecidability.Gordon.LeftNormalForm.alphaLetter k = ⟨Undecidability.MillerTancer.LeftNormalForm.LeftIndex.alpha, FreeGroup.of () ^ k⟩

def Undecidability.Gordon.LeftNormalForm.betaLetter {G : Type} (k : ℤ) : (i : MillerTancer.LeftNormalForm.LeftIndex) × MillerTancer.LeftNormalForm.LeftFactor G i

An integer power in the beta factor, paired with its factor label.

Equations

• Undecidability.Gordon.LeftNormalForm.betaLetter k = ⟨Undecidability.MillerTancer.LeftNormalForm.LeftIndex.beta, FreeGroup.of () ^ k⟩

def Undecidability.Gordon.LeftNormalForm.oldLetter {G : Type} (g : G) : (i : MillerTancer.LeftNormalForm.LeftIndex) × MillerTancer.LeftNormalForm.LeftFactor G i

An original-group element paired with its factor label.

Equations

• Undecidability.Gordon.LeftNormalForm.oldLetter g = ⟨Undecidability.MillerTancer.LeftNormalForm.LeftIndex.old, g⟩

inductive Undecidability.Gordon.LeftNormalForm.LetterCode : Type

The possible endpoint letters, recorded independently of the original group.

• oldW : LetterCode
• oldWInv : LetterCode
• alpha (k : ℤ) : LetterCode
• beta (k : ℤ) : LetterCode

def Undecidability.Gordon.LeftNormalForm.codeLetter {G : Type} [Group G] (w : G) : LetterCode → (i : MillerTancer.LeftNormalForm.LeftIndex) × MillerTancer.LeftNormalForm.LeftFactor G i

The group-valued endpoint letter represented by a letter code.

Equations

• Undecidability.Gordon.LeftNormalForm.codeLetter w Undecidability.Gordon.LeftNormalForm.LetterCode.oldW = Undecidability.Gordon.LeftNormalForm.oldLetter w
• Undecidability.Gordon.LeftNormalForm.codeLetter w Undecidability.Gordon.LeftNormalForm.LetterCode.oldWInv = Undecidability.Gordon.LeftNormalForm.oldLetter w⁻¹
• Undecidability.Gordon.LeftNormalForm.codeLetter w (Undecidability.Gordon.LeftNormalForm.LetterCode.alpha k) = Undecidability.Gordon.LeftNormalForm.alphaLetter k
• Undecidability.Gordon.LeftNormalForm.codeLetter w (Undecidability.Gordon.LeftNormalForm.LetterCode.beta k) = Undecidability.Gordon.LeftNormalForm.betaLetter k

def Undecidability.Gordon.LeftNormalForm.expectedHeadCode {d : ℕ} (degree : Fin d → ℕ) (i : BasisIndex d) (k : ℤ) : LetterCode

The code of the initial letter expected for a basis power.

Equations

• One or more equations did not get rendered due to their size.
• Undecidability.Gordon.LeftNormalForm.expectedHeadCode degree Undecidability.Gordon.BasisIndex.conjugateA k = Undecidability.Gordon.LeftNormalForm.LetterCode.alpha 1
• Undecidability.Gordon.LeftNormalForm.expectedHeadCode degree Undecidability.Gordon.BasisIndex.conjugateAlpha k = Undecidability.Gordon.LeftNormalForm.LetterCode.beta 1

def Undecidability.Gordon.LeftNormalForm.expectedLastCode {d : ℕ} (degree : Fin d → ℕ) (i : BasisIndex d) (k : ℤ) : LetterCode

The code of the final letter expected for a basis power.

Equations

• One or more equations did not get rendered due to their size.
• Undecidability.Gordon.LeftNormalForm.expectedLastCode degree Undecidability.Gordon.BasisIndex.conjugateA k = Undecidability.Gordon.LeftNormalForm.LetterCode.alpha (-1)
• Undecidability.Gordon.LeftNormalForm.expectedLastCode degree Undecidability.Gordon.BasisIndex.conjugateAlpha k = Undecidability.Gordon.LeftNormalForm.LetterCode.beta (-1)

def Undecidability.Gordon.LeftNormalForm.expectedHead {d : ℕ} {G : Type} [Group G] (degree : Fin d → ℕ) (w : G) (i : BasisIndex d) (k : ℤ) : (i : MillerTancer.LeftNormalForm.LeftIndex) × MillerTancer.LeftNormalForm.LeftFactor G i

The group-valued initial letter expected for a basis power.

Equations

• Undecidability.Gordon.LeftNormalForm.expectedHead degree w i k = Undecidability.Gordon.LeftNormalForm.codeLetter w (Undecidability.Gordon.LeftNormalForm.expectedHeadCode degree i k)

def Undecidability.Gordon.LeftNormalForm.expectedLast {d : ℕ} {G : Type} [Group G] (degree : Fin d → ℕ) (w : G) (i : BasisIndex d) (k : ℤ) : (i : MillerTancer.LeftNormalForm.LeftIndex) × MillerTancer.LeftNormalForm.LeftFactor G i

The group-valued final letter expected for a basis power.

Equations

• Undecidability.Gordon.LeftNormalForm.expectedLast degree w i k = Undecidability.Gordon.LeftNormalForm.codeLetter w (Undecidability.Gordon.LeftNormalForm.expectedLastCode degree i k)

@[simp]

theorem Undecidability.Gordon.LeftNormalForm.powerPacked_headLetter {d : ℕ} {G : Type} [Group G] (degree : Fin d → ℕ) (hdegree : ∀ (i : Fin d), 0 < degree i) (x : Fin d → G) (w : G) (hw : w ≠ 1) (i : BasisIndex d) (k : ℤ) (hk : k ≠ 0) : (powerPacked degree hdegree x w hw i k hk).headLetter = expectedHead degree w i k

@[simp]

theorem Undecidability.Gordon.LeftNormalForm.powerPacked_lastLetter {d : ℕ} {G : Type} [Group G] (degree : Fin d → ℕ) (hdegree : ∀ (i : Fin d), 0 < degree i) (x : Fin d → G) (w : G) (hw : w ≠ 1) (i : BasisIndex d) (k : ℤ) (hk : k ≠ 0) : (powerPacked degree hdegree x w hw i k hk).lastLetter = expectedLast degree w i k

@[simp]

theorem Undecidability.Gordon.LeftNormalForm.powerPacked_prod {d : ℕ} {G : Type} [Group G] (degree : Fin d → ℕ) (hdegree : ∀ (i : Fin d), 0 < degree i) (x : Fin d → G) (w : G) (hw : w ≠ 1) (i : BasisIndex d) (k : ℤ) (hk : k ≠ 0) : (powerPacked degree hdegree x w hw i k hk).word.prod = splitBasis degree x w i ^ k

def Undecidability.Gordon.LeftNormalForm.Noncancelling {G : Type} [Group G] (p q : (i : MillerTancer.LeftNormalForm.LeftIndex) × MillerTancer.LeftNormalForm.LeftFactor G i) : Prop

Two adjacent letters do not multiply to the identity when their factor labels agree.

Equations

• Undecidability.Gordon.LeftNormalForm.Noncancelling p q = ∀ (h : p.fst = q.fst), p.snd * cast ⋯ q.snd ≠ 1

theorem Undecidability.Gordon.LeftNormalForm.noncancelling_of_index_ne {G : Type} [Group G] (p q : (i : MillerTancer.LeftNormalForm.LeftIndex) × MillerTancer.LeftNormalForm.LeftFactor G i) (h : p.fst ≠ q.fst) : Noncancelling p q

theorem Undecidability.Gordon.LeftNormalForm.alphaLetter_noncancelling {G : Type} [Group G] (r s : ℤ) (h : r + s ≠ 0) : Noncancelling (alphaLetter r) (alphaLetter s)

theorem Undecidability.Gordon.LeftNormalForm.betaLetter_noncancelling {G : Type} [Group G] (r s : ℤ) (h : r + s ≠ 0) : Noncancelling (betaLetter r) (betaLetter s)

def Undecidability.Gordon.LeftNormalForm.CodeNoncancelling : LetterCode → LetterCode → Prop

The endpoint codes ensure that the corresponding adjacent letters do not cancel.

Equations

• Undecidability.Gordon.LeftNormalForm.CodeNoncancelling (Undecidability.Gordon.LeftNormalForm.LetterCode.alpha r) (Undecidability.Gordon.LeftNormalForm.LetterCode.alpha s) = (r + s ≠ 0)
• Undecidability.Gordon.LeftNormalForm.CodeNoncancelling (Undecidability.Gordon.LeftNormalForm.LetterCode.beta r) (Undecidability.Gordon.LeftNormalForm.LetterCode.beta s) = (r + s ≠ 0)
• Undecidability.Gordon.LeftNormalForm.CodeNoncancelling Undecidability.Gordon.LeftNormalForm.LetterCode.oldW Undecidability.Gordon.LeftNormalForm.LetterCode.oldW = False
• Undecidability.Gordon.LeftNormalForm.CodeNoncancelling Undecidability.Gordon.LeftNormalForm.LetterCode.oldW Undecidability.Gordon.LeftNormalForm.LetterCode.oldWInv = False
• Undecidability.Gordon.LeftNormalForm.CodeNoncancelling Undecidability.Gordon.LeftNormalForm.LetterCode.oldWInv Undecidability.Gordon.LeftNormalForm.LetterCode.oldW = False
• Undecidability.Gordon.LeftNormalForm.CodeNoncancelling Undecidability.Gordon.LeftNormalForm.LetterCode.oldWInv Undecidability.Gordon.LeftNormalForm.LetterCode.oldWInv = False
• Undecidability.Gordon.LeftNormalForm.CodeNoncancelling x✝¹ x✝ = True

theorem Undecidability.Gordon.LeftNormalForm.code_noncancelling {G : Type} [Group G] (w : G) (p q : LetterCode) (h : CodeNoncancelling p q) : Noncancelling (codeLetter w p) (codeLetter w q)

theorem Undecidability.Gordon.LeftNormalForm.expected_noncancelling {d : ℕ} {G : Type} [Group G] (degree : Fin d → ℕ) (hinjective : Function.Injective degree) (w : G) (i j : BasisIndex d) (r s : ℤ) (hij : i ≠ j) : Noncancelling (expectedLast degree w i r) (expectedHead degree w j s)

@[reducible, inline]

abbrev Undecidability.Gordon.LeftNormalForm.IsAppend {G : Type} [Group G] {i j : MillerTancer.LeftNormalForm.LeftIndex} (w : Monoid.CoprodI.NeWord (MillerTancer.LeftNormalForm.LeftFactor G) i j) : Prop

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

Equations

• Undecidability.Gordon.LeftNormalForm.IsAppend w = w.IsAppend

theorem Undecidability.Gordon.LeftNormalForm.positivePowerWord_isAppend {G : Type} [Group G] {i j : MillerTancer.LeftNormalForm.LeftIndex} (u : Monoid.CoprodI.NeWord (MillerTancer.LeftNormalForm.LeftFactor G) i j) (hij : j ≠ i) (n : ℕ) (hu : IsAppend u) : IsAppend (MillerTancer.LeftNormalForm.positivePowerWord u hij n)

theorem Undecidability.Gordon.LeftNormalForm.inv_isAppend {G : Type} [Group G] {i j : MillerTancer.LeftNormalForm.LeftIndex} (u : Monoid.CoprodI.NeWord (MillerTancer.LeftNormalForm.LeftFactor G) i j) (hu : IsAppend u) : IsAppend u.inv

theorem Undecidability.Gordon.LeftNormalForm.cyclicPowerPacked_isAppend {G : Type} [Group G] {i j : MillerTancer.LeftNormalForm.LeftIndex} (u : Monoid.CoprodI.NeWord (MillerTancer.LeftNormalForm.LeftFactor G) i j) (hij : j ≠ i) (k : ℤ) (hk : k ≠ 0) (hu : IsAppend u) : IsAppend (cyclicPowerPacked u hij k hk).word

theorem Undecidability.Gordon.LeftNormalForm.oldBlock_isAppend {d : ℕ} {G : Type} [Group G] (degree : Fin d → ℕ) (hdegree : ∀ (i : Fin d), 0 < degree i) (x : Fin d → G) (i : Fin d) : IsAppend (oldBlock degree hdegree x i)

theorem Undecidability.Gordon.LeftNormalForm.powerPacked_isAppend {d : ℕ} {G : Type} [Group G] (degree : Fin d → ℕ) (hdegree : ∀ (i : Fin d), 0 < degree i) (x : Fin d → G) (w : G) (hw : w ≠ 1) (i : BasisIndex d) (k : ℤ) (hk : k ≠ 0) : IsAppend (powerPacked degree hdegree x w hw i k hk).word

theorem Undecidability.Gordon.LeftNormalForm.exists_joinPacked {G : Type} [Group G] (u v : PackedWord G) (hu : IsAppend u.word) (h : Noncancelling u.lastLetter v.headLetter) : ∃ (q : PackedWord G), q.word.prod = u.word.prod * v.word.prod ∧ q.headLetter = u.headLetter

noncomputable def Undecidability.Gordon.LeftNormalForm.joinPacked {G : Type} [Group G] (u v : PackedWord G) (hu : IsAppend u.word) (h : Noncancelling u.lastLetter v.headLetter) : PackedWord G

The reduced concatenation of two packaged words whose boundary does not cancel.

Equations

• Undecidability.Gordon.LeftNormalForm.joinPacked u v hu h = Classical.choose ⋯

theorem Undecidability.Gordon.LeftNormalForm.joinPacked_prod {G : Type} [Group G] (u v : PackedWord G) (hu : IsAppend u.word) (h : Noncancelling u.lastLetter v.headLetter) : (joinPacked u v hu h).word.prod = u.word.prod * v.word.prod

@[simp]

theorem Undecidability.Gordon.LeftNormalForm.joinPacked_headLetter {G : Type} [Group G] (u v : PackedWord G) (hu : IsAppend u.word) (h : Noncancelling u.lastLetter v.headLetter) : (joinPacked u v hu h).headLetter = u.headLetter

def Undecidability.Gordon.LeftNormalForm.evalBasis {d : ℕ} {G : Type} [Group G] (degree : Fin d → ℕ) (x : Fin d → G) (w : G) : List (BasisIndex d × ℤ) → SplitLeft G

The product of the indicated powers of the proposed basis elements.

Equations

• One or more equations did not get rendered due to their size.
• Undecidability.Gordon.LeftNormalForm.evalBasis degree x w [] = 1

structure Undecidability.Gordon.LeftNormalForm.Image {d : ℕ} {G : Type} [Group G] (degree : Fin d → ℕ) (x : Fin d → G) (w : G) (p : BasisIndex d × ℤ) (rest : List (BasisIndex d × ℤ)) : Type

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

• packed : PackedWord G

  The reduced word together with its endpoint labels.

• prod_eq : self.packed.word.prod = evalBasis degree x w (p :: rest)
• head_eq : self.packed.headLetter = expectedHead degree w p.1 p.2

noncomputable def Undecidability.Gordon.LeftNormalForm.singletonImage {d : ℕ} {G : Type} [Group G] (degree : Fin d → ℕ) (hdegree : ∀ (i : Fin d), 0 < degree i) (x : Fin d → G) (w : G) (hw : w ≠ 1) (i : BasisIndex d) (k : ℤ) (hk : k ≠ 0) : Image degree x w (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.Gordon.LeftNormalForm.mergedImage {d : ℕ} {G : Type} [Group G] (degree : Fin d → ℕ) (hdegree : ∀ (i : Fin d), 0 < degree i) (hinjective : Function.Injective degree) (x : Fin d → G) (w : G) (hw : w ≠ 1) (i j : BasisIndex d) (r s : ℤ) (hr : r ≠ 0) (rest : List (BasisIndex d × ℤ)) (tail : Image degree x w (j, s) rest) (hij : i ≠ j) : Image degree x w (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.

noncomputable def Undecidability.Gordon.LeftNormalForm.imageList {d : ℕ} {G : Type} [Group G] (degree : Fin d → ℕ) (hdegree : ∀ (i : Fin d), 0 < degree i) (hinjective : Function.Injective degree) (x : Fin d → G) (w : G) (hw : w ≠ 1) (p : BasisIndex d × ℤ) (rest : List (BasisIndex d × ℤ)) (hp : p.2 ≠ 0) (hrest : ∀ q ∈ rest, q.2 ≠ 0) (hchain : List.IsChain (fun (a b : BasisIndex d × ℤ) => a.1 ≠ b.1) (p :: rest)) : Image degree x w p rest

The reduced image of a nonempty list of basis powers with noncancelling boundaries.

Equations

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

theorem Undecidability.Gordon.LeftNormalForm.splitBasis_lift_injective {d : ℕ} {G : Type} [Group G] (degree : Fin d → ℕ) (hdegree : ∀ (i : Fin d), 0 < degree i) (hinjective : Function.Injective degree) (x : Fin d → G) (w : G) (hw : w ≠ 1) : Function.Injective ⇑(FreeGroup.lift (splitBasis degree x w))

Gordon's left-hand words freely generate whenever the degree assignment is positive and injective and the parameter word is nontrivial.