2607.20401v1 / ConjugatorLength/Heisenberg.lean
all files
import Mathlib
/-!
# Conjugator length in the integral Heisenberg group
This file formalizes Theorem 4.9 of Bridson--Riley--Sale,
*Conjugator length in finitely presented groups*: the conjugator-length
function of the three-dimensional integral Heisenberg group has quadratic
growth.
The group is first constructed in integer coordinates. We then use literal
words in the six standard signed generators, so the length used below is the
standard word length, rather than a convenient coordinate norm.
-/
namespace ConjugatorLength
/-- Integer coordinates for the matrices
`[[1,x,z],[0,1,y],[0,0,1]]`. -/
@[ext]
structure Heisenberg where
x : ℤ
y : ℤ
z : ℤ
deriving DecidableEq
namespace Heisenberg
instance : One Heisenberg := ⟨⟨0, 0, 0⟩⟩
instance : Mul Heisenberg :=
⟨fun g h => ⟨g.x + h.x, g.y + h.y, g.z + h.z + g.x * h.y⟩⟩
instance : Inv Heisenberg :=
⟨fun g => ⟨-g.x, -g.y, -g.z + g.x * g.y⟩⟩
@[simp] theorem one_x : (1 : Heisenberg).x = 0 := rfl
@[simp] theorem one_y : (1 : Heisenberg).y = 0 := rfl
@[simp] theorem one_z : (1 : Heisenberg).z = 0 := rfl
@[simp] theorem mul_x (g h : Heisenberg) : (g * h).x = g.x + h.x := rfl
@[simp] theorem mul_y (g h : Heisenberg) : (g * h).y = g.y + h.y := rfl
@[simp] theorem mul_z (g h : Heisenberg) : (g * h).z = g.z + h.z + g.x * h.y := rfl
@[simp] theorem inv_x (g : Heisenberg) : g⁻¹.x = -g.x := rfl
@[simp] theorem inv_y (g : Heisenberg) : g⁻¹.y = -g.y := rfl
@[simp] theorem inv_z (g : Heisenberg) : g⁻¹.z = -g.z + g.x * g.y := rfl
instance : Group Heisenberg where
mul_assoc a b c := by ext <;> simp <;> ring
one_mul a := by ext <;> simp
mul_one a := by ext <;> simp
inv_mul_cancel a := by ext <;> simp
/-- The displayed matrix model from the paper. -/
def toMatrix (g : Heisenberg) : Matrix (Fin 3) (Fin 3) ℤ :=
!![1, g.x, g.z; 0, 1, g.y; 0, 0, 1]
/-- Coordinate multiplication really is multiplication of the upper unitriangular
integer matrices displayed in the paper. -/
theorem toMatrix_mul (g h : Heisenberg) :
toMatrix (g * h) = toMatrix g * toMatrix h := by
ext i j
fin_cases i <;> fin_cases j <;>
simp [toMatrix, Matrix.mul_apply, Fin.sum_univ_succ] <;> ring
theorem toMatrix_one : toMatrix 1 = 1 := by
ext i j
fin_cases i <;> fin_cases j <;> simp [toMatrix]
theorem toMatrix_injective : Function.Injective toMatrix := by
intro g h H
ext
· have h01 := congrFun (congrFun H (0 : Fin 3)) (1 : Fin 3)
simpa [toMatrix] using h01
· have h12 := congrFun (congrFun H (1 : Fin 3)) (2 : Fin 3)
simpa [toMatrix] using h12
· have h02 := congrFun (congrFun H (0 : Fin 3)) (2 : Fin 3)
simpa [toMatrix] using h02
/-- The three standard generators. -/
def a : Heisenberg := ⟨1, 0, 0⟩
def b : Heisenberg := ⟨0, 1, 0⟩
def c : Heisenberg := ⟨0, 0, 1⟩
@[simp] theorem a_x : a.x = 1 := rfl
@[simp] theorem a_y : a.y = 0 := rfl
@[simp] theorem a_z : a.z = 0 := rfl
@[simp] theorem b_x : b.x = 0 := rfl
@[simp] theorem b_y : b.y = 1 := rfl
@[simp] theorem b_z : b.z = 0 := rfl
@[simp] theorem c_x : c.x = 0 := rfl
@[simp] theorem c_y : c.y = 0 := rfl
@[simp] theorem c_z : c.z = 1 := rfl
/-- The relator `[a,b]=c` in the paper's commutator convention. -/
theorem commutator_a_b : a⁻¹ * b⁻¹ * a * b = c := by
ext <;> norm_num [a, b, c]
theorem commute_a_c : a * c = c * a := by
ext <;> norm_num [a, c]
theorem commute_b_c : b * c = c * b := by
ext <;> norm_num [b, c]
/-- The six letters in the symmetric standard generating set. -/
inductive Letter
| a | aInv | b | bInv | c | cInv
deriving DecidableEq
instance : Fintype Letter where
elems := {.a, .aInv, .b, .bInv, .c, .cInv}
complete x := by cases x <;> simp
/-- Interpretation of a signed generator as a Heisenberg element. -/
def Letter.val : Letter → Heisenberg
| .a => Heisenberg.a
| .aInv => Heisenberg.a⁻¹
| .b => Heisenberg.b
| .bInv => Heisenberg.b⁻¹
| .c => Heisenberg.c
| .cInv => Heisenberg.c⁻¹
@[simp] theorem Letter.val_a : Letter.a.val = Heisenberg.a := rfl
@[simp] theorem Letter.val_aInv : Letter.aInv.val = Heisenberg.a⁻¹ := rfl
@[simp] theorem Letter.val_b : Letter.b.val = Heisenberg.b := rfl
@[simp] theorem Letter.val_bInv : Letter.bInv.val = Heisenberg.b⁻¹ := rfl
@[simp] theorem Letter.val_c : Letter.c.val = Heisenberg.c := rfl
@[simp] theorem Letter.val_cInv : Letter.cInv.val = Heisenberg.c⁻¹ := rfl
/-- Evaluation of a literal word. -/
def eval (w : List Letter) : Heisenberg := (w.map Letter.val).prod
@[simp] theorem eval_nil : eval [] = 1 := rfl
@[simp] theorem eval_cons (s : Letter) (w : List Letter) :
eval (s :: w) = s.val * eval w := by
simp [eval]
/-- A word spelling an integral power, by repeating a positive or negative
letter. -/
def intWord (pos neg : Letter) : ℤ → List Letter
| .ofNat n => List.replicate n pos
| .negSucc n => List.replicate (n + 1) neg
@[simp] theorem length_intWord (pos neg : Letter) (n : ℤ) :
(intWord pos neg n).length = n.natAbs := by
cases n <;> simp [intWord]
@[simp] theorem eval_intWord_a (n : ℤ) :
eval (intWord .a .aInv n) = ⟨n, 0, 0⟩ := by
cases n with
| ofNat n =>
induction n with
| zero => rfl
| succ n ih =>
rw [show intWord .a .aInv (Int.ofNat (n + 1)) =
.a :: intWord .a .aInv (Int.ofNat n) by simp [intWord, List.replicate_succ]]
rw [eval_cons, ih]
ext <;> norm_num [Letter.val, Heisenberg.a] <;> omega
| negSucc n =>
induction n with
| zero =>
ext <;> norm_num [intWord, Letter.val, Heisenberg.a] <;> omega
| succ n ih =>
rw [show intWord .a .aInv (Int.negSucc (n + 1)) =
.aInv :: intWord .a .aInv (Int.negSucc n) by
simp [intWord, List.replicate_succ, Nat.add_assoc]]
rw [eval_cons, ih]
ext <;> norm_num [Letter.val, Heisenberg.a] <;> omega
@[simp] theorem eval_intWord_b (n : ℤ) :
eval (intWord .b .bInv n) = ⟨0, n, 0⟩ := by
cases n with
| ofNat n =>
induction n with
| zero => rfl
| succ n ih =>
rw [show intWord .b .bInv (Int.ofNat (n + 1)) =
.b :: intWord .b .bInv (Int.ofNat n) by simp [intWord, List.replicate_succ]]
rw [eval_cons, ih]
ext <;> norm_num [Letter.val, Heisenberg.b] <;> omega
| negSucc n =>
induction n with
| zero =>
ext <;> norm_num [intWord, Letter.val, Heisenberg.b] <;> omega
| succ n ih =>
rw [show intWord .b .bInv (Int.negSucc (n + 1)) =
.bInv :: intWord .b .bInv (Int.negSucc n) by
simp [intWord, List.replicate_succ, Nat.add_assoc]]
rw [eval_cons, ih]
ext <;> norm_num [Letter.val, Heisenberg.b] <;> omega
@[simp] theorem eval_intWord_c (n : ℤ) :
eval (intWord .c .cInv n) = ⟨0, 0, n⟩ := by
cases n with
| ofNat n =>
induction n with
| zero => rfl
| succ n ih =>
rw [show intWord .c .cInv (Int.ofNat (n + 1)) =
.c :: intWord .c .cInv (Int.ofNat n) by simp [intWord, List.replicate_succ]]
rw [eval_cons, ih]
ext <;> norm_num [Letter.val, Heisenberg.c] <;> omega
| negSucc n =>
induction n with
| zero =>
ext <;> norm_num [intWord, Letter.val, Heisenberg.c] <;> omega
| succ n ih =>
rw [show intWord .c .cInv (Int.negSucc (n + 1)) =
.cInv :: intWord .c .cInv (Int.negSucc n) by
simp [intWord, List.replicate_succ, Nat.add_assoc]]
rw [eval_cons, ih]
ext <;> norm_num [Letter.val, Heisenberg.c] <;> omega
/-- A standard spelling of a coordinate triple. The `b`-block is put before
the `a`-block so that it creates no unwanted central coordinate. -/
def normalWord (g : Heisenberg) : List Letter :=
intWord .b .bInv g.y ++ intWord .a .aInv g.x ++ intWord .c .cInv g.z
@[simp] theorem eval_append (u v : List Letter) :
eval (u ++ v) = eval u * eval v := by
simp [eval]
@[simp] theorem eval_normalWord (g : Heisenberg) : eval (normalWord g) = g := by
ext <;> simp [normalWord]
theorem eval_surjective : Function.Surjective eval :=
fun g => ⟨normalWord g, eval_normalWord g⟩
@[simp] theorem length_normalWord (g : Heisenberg) :
(normalWord g).length = g.y.natAbs + g.x.natAbs + g.z.natAbs := by
simp [normalWord, add_assoc]
/-- The standard word length: the least length of a literal word evaluating
to `g`. -/
noncomputable def wordLength (g : Heisenberg) : ℕ :=
by
classical
exact Nat.find
(show ∃ n : ℕ, ∃ w : List Letter, eval w = g ∧ w.length = n from
⟨(normalWord g).length, normalWord g, eval_normalWord g, rfl⟩)
theorem exists_word_wordLength (g : Heisenberg) :
∃ w : List Letter, eval w = g ∧ w.length = wordLength g := by
classical
exact Nat.find_spec
(show ∃ n : ℕ, ∃ w : List Letter, eval w = g ∧ w.length = n from
⟨(normalWord g).length, normalWord g, eval_normalWord g, rfl⟩)
theorem wordLength_le_of_eval {g : Heisenberg} {w : List Letter} (hw : eval w = g) :
wordLength g ≤ w.length := by
classical
unfold wordLength
apply Nat.find_min'
exact ⟨w, hw, rfl⟩
theorem wordLength_le_normal (g : Heisenberg) :
wordLength g ≤ g.y.natAbs + g.x.natAbs + g.z.natAbs := by
rw [← length_normalWord]
exact wordLength_le_of_eval (eval_normalWord g)
/-- Each horizontal coordinate is bounded by the length of any spelling. -/
theorem eval_x_natAbs_le_length (w : List Letter) :
(eval w).x.natAbs ≤ w.length := by
induction w with
| nil => simp
| cons s w ih =>
rw [eval_cons, mul_x, List.length_cons]
calc
(s.val.x + (eval w).x).natAbs
≤ s.val.x.natAbs + (eval w).x.natAbs := Int.natAbs_add_le _ _
_ ≤ 1 + w.length := by
apply Nat.add_le_add
· cases s <;> norm_num [Letter.val, Heisenberg.a, Heisenberg.b, Heisenberg.c]
· exact ih
_ = w.length + 1 := by omega
theorem eval_y_natAbs_le_length (w : List Letter) :
(eval w).y.natAbs ≤ w.length := by
induction w with
| nil => simp
| cons s w ih =>
rw [eval_cons, mul_y, List.length_cons]
calc
(s.val.y + (eval w).y).natAbs
≤ s.val.y.natAbs + (eval w).y.natAbs := Int.natAbs_add_le _ _
_ ≤ 1 + w.length := by
apply Nat.add_le_add
· cases s <;> norm_num [Letter.val, Heisenberg.a, Heisenberg.b, Heisenberg.c]
· exact ih
_ = w.length + 1 := by omega
/-- The central coordinate of a length `n` word has size at most `n²`. -/
theorem eval_z_natAbs_le_length_sq (w : List Letter) :
(eval w).z.natAbs ≤ w.length ^ 2 := by
induction w with
| nil => simp
| cons s w ih =>
rw [eval_cons, mul_z, List.length_cons]
have hsx : s.val.x.natAbs ≤ 1 := by
cases s <;> norm_num [Letter.val, Heisenberg.a, Heisenberg.b, Heisenberg.c]
have hsz : s.val.z.natAbs ≤ 1 := by
cases s <;> norm_num [Letter.val, Heisenberg.a, Heisenberg.b, Heisenberg.c]
have hy := eval_y_natAbs_le_length w
calc
(s.val.z + (eval w).z + s.val.x * (eval w).y).natAbs
≤ (s.val.z + (eval w).z).natAbs +
(s.val.x * (eval w).y).natAbs := Int.natAbs_add_le _ _
_ ≤ (s.val.z.natAbs + (eval w).z.natAbs) +
s.val.x.natAbs * (eval w).y.natAbs := by
rw [Int.natAbs_mul]
exact Nat.add_le_add_right (Int.natAbs_add_le _ _) _
_ ≤ (1 + w.length ^ 2) + 1 * w.length := by
gcongr
_ ≤ (w.length + 1) ^ 2 := by nlinarith
theorem x_natAbs_le_wordLength (g : Heisenberg) :
g.x.natAbs ≤ wordLength g := by
obtain ⟨w, hw, hlen⟩ := exists_word_wordLength g
simpa [hw, hlen] using eval_x_natAbs_le_length w
theorem y_natAbs_le_wordLength (g : Heisenberg) :
g.y.natAbs ≤ wordLength g := by
obtain ⟨w, hw, hlen⟩ := exists_word_wordLength g
simpa [hw, hlen] using eval_y_natAbs_le_length w
theorem z_natAbs_le_wordLength_sq (g : Heisenberg) :
g.z.natAbs ≤ wordLength g ^ 2 := by
obtain ⟨w, hw, hlen⟩ := exists_word_wordLength g
simpa [hw, hlen] using eval_z_natAbs_le_length_sq w
/-- The paper's equation `u w = w v`. -/
def IsConjugator (u v w : Heisenberg) : Prop := u * w = w * v
/-- Conjugacy phrased in the convention used to define conjugator length. -/
def Conjugate (u v : Heisenberg) : Prop := ∃ w, IsConjugator u v w
theorem conjugate_iff_isConj {u v : Heisenberg} :
Conjugate u v ↔ IsConj u v := by
constructor
· rintro ⟨w, hw⟩
rw [isConj_iff]
refine ⟨w⁻¹, ?_⟩
dsimp [IsConjugator] at hw
calc
w⁻¹ * u * (w⁻¹)⁻¹ = w⁻¹ * (u * w) := by simp [mul_assoc]
_ = w⁻¹ * (w * v) := by rw [hw]
_ = v := by simp
· intro h
rw [isConj_iff] at h
obtain ⟨k, hk⟩ := h
refine ⟨k⁻¹, ?_⟩
dsimp [IsConjugator]
calc
u * k⁻¹ = k⁻¹ * (k * u * k⁻¹) := by simp [mul_assoc]
_ = k⁻¹ * v := by rw [hk]
/-- Coordinate form of the conjugator equation (equation (6) in the paper). -/
theorem isConjugator_iff (u v w : Heisenberg) :
IsConjugator u v w ↔
u.x = v.x ∧ u.y = v.y ∧ v.y * w.x - u.x * w.y = u.z - v.z := by
constructor
· intro h
have hx := congrArg Heisenberg.x h
have hy := congrArg Heisenberg.y h
have hz := congrArg Heisenberg.z h
simp only [mul_x] at hx
simp only [mul_y] at hy
simp only [mul_z] at hz
have hx' : u.x = v.x := by omega
have hy' : u.y = v.y := by omega
constructor
· exact hx'
constructor
· exact hy'
· linarith
· rintro ⟨hx, hy, hz⟩
ext
· simp [hx, add_comm]
· simp [hy, add_comm]
· simp only [mul_z]
rw [hx] at hz ⊢
linear_combination -hz
/-- A deliberately elementary bounded-solution lemma for the one-row
Diophantine equation used in the conjugacy calculation. This slightly weaker
bound than Lemma 4.10 of the paper is ample for quadratic growth. -/
theorem bounded_diophantine_solution {A B C x y : ℤ}
(h : A * x + B * y = C) :
∃ x' y' : ℤ, A * x' + B * y' = C ∧
x'.natAbs ≤ B.natAbs + C.natAbs ∧
y'.natAbs ≤ C.natAbs + A.natAbs * B.natAbs := by
by_cases hB : B = 0
· subst B
simp only [zero_mul, add_zero] at h ⊢
by_cases hA : A = 0
· subst A
simp at h
subst C
exact ⟨0, 0, by simp⟩
· refine ⟨x, 0, h, ?_, by simp⟩
have hAn : 1 ≤ A.natAbs := (Int.natAbs_pos.mpr hA)
have habs : C.natAbs = A.natAbs * x.natAbs := by
rw [← h, Int.natAbs_mul]
calc
x.natAbs = 1 * x.natAbs := by simp
_ ≤ A.natAbs * x.natAbs := Nat.mul_le_mul_right _ hAn
_ = C.natAbs := habs.symm
_ ≤ (0 : ℤ).natAbs + C.natAbs := by simp
· let x' : ℤ := x % B
let y' : ℤ := y + A * (x / B)
refine ⟨x', y', ?_, ?_, ?_⟩
· dsimp [x', y']
calc
A * (x % B) + B * (y + A * (x / B))
= A * (x / B * B + x % B) + B * y := by ring
_ = A * x + B * y := by rw [Int.ediv_mul_add_emod]
_ = C := h
· dsimp [x']
have hxnonneg : 0 ≤ x % B := Int.emod_nonneg _ hB
have hxlt : x % B < (B.natAbs : ℤ) := Int.emod_lt _ hB
rw [← Int.natAbs_of_nonneg hxnonneg] at hxlt
omega
· have heq : B * y' = C - A * x' := by
have hxy : A * x' + B * y' = C := by
dsimp [x', y']
calc
A * (x % B) + B * (y + A * (x / B))
= A * (x / B * B + x % B) + B * y := by ring
_ = A * x + B * y := by rw [Int.ediv_mul_add_emod]
_ = C := h
linarith
have hprod :
B.natAbs * y'.natAbs = (C - A * x').natAbs := by
rw [← Int.natAbs_mul, heq]
have hBnat : 1 ≤ B.natAbs := Int.natAbs_pos.mpr hB
have hxbound : x'.natAbs ≤ B.natAbs := by
dsimp [x']
have hxnonneg : 0 ≤ x % B := Int.emod_nonneg _ hB
have hxlt : x % B < (B.natAbs : ℤ) := Int.emod_lt _ hB
rw [← Int.natAbs_of_nonneg hxnonneg] at hxlt
omega
calc
y'.natAbs = 1 * y'.natAbs := by simp
_ ≤ B.natAbs * y'.natAbs := Nat.mul_le_mul_right _ hBnat
_ = (C - A * x').natAbs := hprod
_ ≤ C.natAbs + (A * x').natAbs := Int.natAbs_sub_le _ _
_ = C.natAbs + A.natAbs * x'.natAbs := by rw [Int.natAbs_mul]
_ ≤ C.natAbs + A.natAbs * B.natAbs := by gcongr
/-- A quadratic upper bound for an individual conjugacy instance, measured
using the actual standard word metric. -/
theorem exists_conjugator_wordLength_le {u v : Heisenberg} {n : ℕ}
(huv : Conjugate u v) (hlen : wordLength u + wordLength v ≤ n) :
∃ w, IsConjugator u v w ∧ wordLength w ≤ 4 * n ^ 2 := by
obtain ⟨w₀, hw₀⟩ := huv
have hcoord := (isConjugator_iff u v w₀).mp hw₀
obtain ⟨x, y, hxy, hx, hy⟩ :=
bounded_diophantine_solution
(A := v.y) (B := -u.x) (C := u.z - v.z)
(x := w₀.x) (y := w₀.y) (by simpa [sub_eq_add_neg] using hcoord.2.2)
let w : Heisenberg := ⟨x, y, 0⟩
refine ⟨w, ?_, ?_⟩
· apply (isConjugator_iff u v w).mpr
refine ⟨hcoord.1, hcoord.2.1, ?_⟩
simpa [w, sub_eq_add_neg] using hxy
· have hux : u.x.natAbs ≤ wordLength u := x_natAbs_le_wordLength u
have hvy : v.y.natAbs ≤ wordLength v := y_natAbs_le_wordLength v
have huz : u.z.natAbs ≤ wordLength u ^ 2 := z_natAbs_le_wordLength_sq u
have hvz : v.z.natAbs ≤ wordLength v ^ 2 := z_natAbs_le_wordLength_sq v
have hC : (u.z - v.z).natAbs ≤ n ^ 2 := by
calc
(u.z - v.z).natAbs ≤ u.z.natAbs + v.z.natAbs := Int.natAbs_sub_le _ _
_ ≤ wordLength u ^ 2 + wordLength v ^ 2 := Nat.add_le_add huz hvz
_ ≤ (wordLength u + wordLength v) ^ 2 := by nlinarith
_ ≤ n ^ 2 := Nat.pow_le_pow_left hlen 2
have huxn : u.x.natAbs ≤ n := le_trans hux (le_trans (Nat.le_add_right _ _) hlen)
have hvyn : v.y.natAbs ≤ n :=
le_trans hvy (le_trans (Nat.le_add_left _ _) hlen)
have huxnegn : (-u.x).natAbs ≤ n := by simpa using huxn
have hx' : x.natAbs ≤ n + n ^ 2 := by
exact le_trans hx (Nat.add_le_add huxnegn hC)
have hy' : y.natAbs ≤ n ^ 2 + n * n := by
calc
y.natAbs ≤ (u.z - v.z).natAbs + v.y.natAbs * (-u.x).natAbs := hy
_ ≤ n ^ 2 + n * n := by
rw [Int.natAbs_neg]
gcongr
have hn : n ≤ n ^ 2 := by
cases n with
| zero => simp
| succ n => simp only [pow_two]; nlinarith
calc
wordLength w ≤ w.y.natAbs + w.x.natAbs + w.z.natAbs :=
wordLength_le_normal w
_ = y.natAbs + x.natAbs := by simp [w]
_ ≤ (n ^ 2 + n * n) + (n + n ^ 2) := Nat.add_le_add hy' hx'
_ ≤ 4 * n ^ 2 := by
simp only [pow_two] at hn ⊢
nlinarith
/-- The lower-bound pair in integer coordinates. -/
def lowerU (n : ℕ) : Heisenberg := ⟨0, 1, (n : ℤ) ^ 2⟩
def lowerV : Heisenberg := b
theorem lower_conjugate (n : ℕ) : Conjugate (lowerU n) lowerV := by
refine ⟨⟨(n : ℤ) ^ 2, 0, 0⟩, ?_⟩
rw [isConjugator_iff]
norm_num [lowerU, lowerV, b]
theorem lower_conjugator_x {n : ℕ} {w : Heisenberg}
(hw : IsConjugator (lowerU n) lowerV w) :
w.x = (n : ℤ) ^ 2 := by
have h := (isConjugator_iff (lowerU n) lowerV w).mp hw
norm_num [lowerU, lowerV, b] at h
exact h
theorem lower_wordLength {n : ℕ} {w : Heisenberg}
(hw : IsConjugator (lowerU n) lowerV w) :
n ^ 2 ≤ wordLength w := by
have hx := x_natAbs_le_wordLength w
rw [lower_conjugator_x hw] at hx
norm_num [Int.natAbs_pow] at hx
simpa using hx
/-- A literal word of length `4n+1` representing `lowerU n`: it is
`b [a^n,b^n]`. -/
def lowerUWord (n : ℕ) : List Letter :=
[.b] ++
intWord .a .aInv (-(n : ℤ)) ++
intWord .b .bInv (-(n : ℤ)) ++
intWord .a .aInv (n : ℤ) ++
intWord .b .bInv (n : ℤ)
def lowerVWord : List Letter := [.b]
@[simp] theorem length_lowerUWord (n : ℕ) : (lowerUWord n).length = 4 * n + 1 := by
simp [lowerUWord]
omega
@[simp] theorem length_lowerVWord : lowerVWord.length = 1 := rfl
@[simp] theorem eval_lowerUWord (n : ℕ) : eval (lowerUWord n) = lowerU n := by
ext <;> simp [lowerUWord, lowerU, Letter.val, Heisenberg.b] <;> ring
@[simp] theorem eval_lowerVWord : eval lowerVWord = lowerV := by
simp [lowerVWord, lowerV, Letter.val]
end Heisenberg
end ConjugatorLength