The binary tree, its automorphisms, and the Grigorchuk group

Definition

Garrido_Grigorchuk

by dbenbenn · Sep 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

grigorchuk-groupgroup-theorygrowth

The rooted binary tree, its automorphisms, and the (first) Grigorchuk group $\Gamma$ .

The tree. p. 13 (Definition 4.6): “Denote by $T$ the infinite rooted binary tree. We will generally identify the vertices of $T$ with finite words in the alphabet $\{0, 1\}$ .” p. 14: “For any vertex $v$ of $T$ , there is a unique path to the root. The level of $v$ is the number of edges in this unique path to the root.” The vertices are these words, as List Bool (with false $= 0$ and true $= 1$ ); the root is the empty word, the level of a vertex is its length, and $v$ lies below $u$ when $u$ is a prefix of $v$ .

BinaryTreeAut. The source uses the automorphisms of $T$ without defining them (Definition 4.6, p. 13). Here they are the permutations of the vertices that preserve length and the prefix order in both directions. They form a group under composition.

The generators. p. 13 (Definition 4.6): “The automorphism $a$ rigidly swaps the two subtrees $T_0, T_1$ rooted at the first level of $T$ , while $b, c$ and $d$ leave the first level intact and are defined recursively by $b = (a, c), c = (a, d), d = (1, b)$ . This notation means that, for instance, $b$ acts on $T_0$ (the subtree rooted at the leftmost vertex of the first level) like $a$ acts on $T$ , while acting on $T_1$ like $c$ does on $T$ .” Here $a$ changes the first letter of every nonempty word, and $b$ , $c$ , $d$ fix the first letter and act on what follows by this recursion: on $0w$ and $1w$ ,

b(0w) = 0\,a(w),\ b(1w) = 1\,c(w),\quad c(0w) = 0\,a(w),\ c(1w) = 1\,d(w),\quad d(0w) = 0w,\ d(1w) = 1\,b(w).

Each is shown to be an involutive automorphism of $T$ .

GrigorchukGroup. p. 13 (Definition 4.6): “The (first) Grigorchuk group $\Gamma$ is a group of automorphisms of $T$ generated by four automorphisms denoted $a, b, c, d$ .” Here $\Gamma$ is the subgroup of the automorphisms of $T$ generated by $a, b, c, d$ ; GrigorchukGroup.a, …, GrigorchukGroup.d are the generators as elements of $\Gamma$ , and GrigorchukGroup.generators is the set $S = \{a, b, c, d\}$ .

levelStabilizer $n$ . p. 14: “The stabilizer of $v$ is denoted by $St(v)$ and the $n$ th level stabilizer $St(n)$ is the intersection of the stabilizers of all vertices of level $n$ .” Here $St(n)$ is the set of elements of $\Gamma$ fixing every vertex of level $n$ .

treeSection $g$ $v$ . The source has no defining sentence for the section of an arbitrary automorphism at an arbitrary vertex; it reaches sections only through the maps of the Remark, p. 14: “To see this, define $\varphi_0, \varphi_1 : St(1) \to \Gamma$ by $\varphi_0(g_0, g_1) = g_0$ , $\varphi_1(g_0, g_1) = g_1$ .” The section $g|_v$ of an automorphism $g$ at a vertex $v$ is the automorphism of $T$ describing how $g$ acts below $v$ , defined by $g(v w) = g(v)\, g|_v(w)$ ; at the two first-level vertices these are the components that $\varphi_0, \varphi_1$ pick out. p. 14 (Lemma 4.8): “For each $g \in St(3)$ we have $\sum_{i,j,k=0,1} l(g_{ijk}) \le \frac{3}{4} l(g) + 8$ , where $g_{ijk}$ is the element obtained by reducing $\varphi_k(\varphi_j(\varphi_i(g)))$ .” The section at the level-3 vertex $ijk$ is this $g_{ijk}$ .

stOnePair. p. 14: “Writing any element $u \in St(1)$ as $u = (u_0, u_1)$ , it is easy to see that conjugation by $a$ , induces a ‘swapped’ action: $aua = (u_1, u_0)$ .” p. 14 (Remark): “This also shows that the map $\psi : St(1) \to \Gamma \times \Gamma$ , $g \mapsto (g_0, g_1)$ is a monomorphism.” Here $u_0$ and $u_1$ are the sections of $u$ at the two first-level vertices; that notation, $u \mapsto (u_0, u_1)$ , is stOnePair, defined, as in the notes, on $St(1)$ only. Its values are pairs of automorphisms of $T$ (as the sections in treeSection are automorphisms of $T$ , where the source's $\varphi_i$ land in $\Gamma$ ); that they lie in $\Gamma$ and that the map is multiplicative is a statement of the mission.

wordLength. p. 14 (§4.2.1): “Throughout, we will abuse notation and write $l(g)$ to mean both the length of a shortest word representing $g$ and for the length of $g$ as a word.” Here $l(g)$ for $g \in \Gamma$ is the least $n$ such that $g$ is a product of at most $n$ elements of $S \cup S^{-1}$ (the imported Chou.wordBall). It is defined as an infimum, which would be $0$ for an element in no ball; that does not arise, because $a, b, c, d$ generate $\Gamma$ and so every element lies in some ball.

Definition code

import Mathlib
import Definitions.Def_Chou_Growth

namespace Garrido

/-- The automorphisms of the rooted binary tree: permutations of the finite words in `{0, 1}`
(`false` = 0, `true` = 1) that preserve length and the prefix order in both directions. -/
def BinaryTreeAut : Subgroup (Equiv.Perm (List Bool)) where
  carrier := {σ | (∀ v : List Bool, (σ v).length = v.length) ∧
    ∀ v w : List Bool, v <+: w ↔ σ v <+: σ w}
  mul_mem' := by
    rintro σ τ ⟨hσl, hσ⟩ ⟨hτl, hτ⟩
    refine ⟨fun v => ?_, fun v w => ?_⟩
    · simp [hσl, hτl]
    · simp only [Equiv.Perm.coe_mul, Function.comp_apply]
      rw [hτ v w, hσ]
  one_mem' := ⟨fun v => rfl, fun v w => Iff.rfl⟩
  inv_mem' := by
    rintro σ ⟨hσl, hσ⟩
    refine ⟨fun v => ?_, fun v w => ?_⟩
    · have := hσl (σ⁻¹ v); simp at this; exact this.symm
    · rw [hσ (σ⁻¹ v) (σ⁻¹ w)]; simp

/-- `a` exchanges the two subtrees below the root: it changes the first letter. -/
def grigAFun : List Bool → List Bool
  | [] => []
  | x :: w => (!x) :: w

mutual
/-- `b = (a, c)`. -/
def grigBFun : List Bool → List Bool
  | [] => []
  | false :: w => false :: grigAFun w
  | true :: w => true :: grigCFun w
/-- `c = (a, d)`. -/
def grigCFun : List Bool → List Bool
  | [] => []
  | false :: w => false :: grigAFun w
  | true :: w => true :: grigDFun w
/-- `d = (1, b)`. -/
def grigDFun : List Bool → List Bool
  | [] => []
  | false :: w => false :: w
  | true :: w => true :: grigBFun w
end

theorem grigAFun_involutive : Function.Involutive grigAFun := by
  intro w; cases w <;> simp [grigAFun]

theorem grigBCD_involutive (w : List Bool) :
    grigBFun (grigBFun w) = w ∧ grigCFun (grigCFun w) = w ∧ grigDFun (grigDFun w) = w := by
  induction w with
  | nil => simp [grigBFun, grigCFun, grigDFun]
  | cons x w ih =>
    cases x <;> simp [grigBFun, grigCFun, grigDFun, grigAFun_involutive w, ih.1, ih.2.1, ih.2.2]

theorem grigAFun_length (w : List Bool) : (grigAFun w).length = w.length := by
  cases w <;> simp [grigAFun]

theorem grigBCD_length (w : List Bool) : (grigBFun w).length = w.length ∧
    (grigCFun w).length = w.length ∧ (grigDFun w).length = w.length := by
  induction w with
  | nil => simp [grigBFun, grigCFun, grigDFun]
  | cons x w ih => cases x <;> simp [grigBFun, grigCFun, grigDFun, grigAFun_length, ih.1, ih.2.1, ih.2.2]

theorem grigAFun_prefix {v w : List Bool} (h : v <+: w) : grigAFun v <+: grigAFun w := by
  obtain ⟨t, rfl⟩ := h
  cases v with
  | nil => simp [grigAFun]
  | cons x v => exact ⟨t, by simp [grigAFun]⟩

theorem grigBCD_prefix (v : List Bool) : ∀ w, v <+: w →
    grigBFun v <+: grigBFun w ∧ grigCFun v <+: grigCFun w ∧ grigDFun v <+: grigDFun w := by
  induction v with
  | nil => intro w _; simp [grigBFun, grigCFun, grigDFun]
  | cons x v ih =>
    intro w h
    obtain ⟨t, rfl⟩ := h
    have ih' := ih (v ++ t) ⟨t, rfl⟩
    cases x <;> simp only [List.cons_append, grigBFun, grigCFun, grigDFun, List.cons_prefix_cons,
      true_and] <;> exact ⟨by first | exact grigAFun_prefix ⟨t, rfl⟩ | exact ih'.2.1,
        by first | exact grigAFun_prefix ⟨t, rfl⟩ | exact ih'.2.2,
        by first | exact ⟨t, rfl⟩ | exact ih'.1⟩


theorem grigAFun_prefix_iff (v w : List Bool) : v <+: w ↔ grigAFun v <+: grigAFun w :=
  ⟨grigAFun_prefix, fun h => by
    simpa [grigAFun_involutive v, grigAFun_involutive w] using grigAFun_prefix h⟩

theorem grigBCD_prefix_iff (v w : List Bool) : (v <+: w ↔ grigBFun v <+: grigBFun w) ∧
    (v <+: w ↔ grigCFun v <+: grigCFun w) ∧ (v <+: w ↔ grigDFun v <+: grigDFun w) := by
  refine ⟨⟨fun h => (grigBCD_prefix v w h).1, fun h => ?_⟩,
    ⟨fun h => (grigBCD_prefix v w h).2.1, fun h => ?_⟩,
    ⟨fun h => (grigBCD_prefix v w h).2.2, fun h => ?_⟩⟩
  · simpa [(grigBCD_involutive v).1, (grigBCD_involutive w).1] using (grigBCD_prefix _ _ h).1
  · simpa [(grigBCD_involutive v).2.1, (grigBCD_involutive w).2.1] using (grigBCD_prefix _ _ h).2.1
  · simpa [(grigBCD_involutive v).2.2, (grigBCD_involutive w).2.2] using (grigBCD_prefix _ _ h).2.2

/-- The generator `a` of the Grigorchuk group, as a tree automorphism. -/
def grigA : BinaryTreeAut :=
  ⟨grigAFun_involutive.toPerm _, grigAFun_length, grigAFun_prefix_iff⟩
/-- The generator `b = (a, c)`. -/
def grigB : BinaryTreeAut :=
  ⟨Function.Involutive.toPerm grigBFun (fun w => (grigBCD_involutive w).1),
    fun w => (grigBCD_length w).1, fun v w => (grigBCD_prefix_iff v w).1⟩
/-- The generator `c = (a, d)`. -/
def grigC : BinaryTreeAut :=
  ⟨Function.Involutive.toPerm grigCFun (fun w => (grigBCD_involutive w).2.1),
    fun w => (grigBCD_length w).2.1, fun v w => (grigBCD_prefix_iff v w).2.1⟩
/-- The generator `d = (1, b)`. -/
def grigD : BinaryTreeAut :=
  ⟨Function.Involutive.toPerm grigDFun (fun w => (grigBCD_involutive w).2.2),
    fun w => (grigBCD_length w).2.2, fun v w => (grigBCD_prefix_iff v w).2.2⟩

/-- The (first) Grigorchuk group `Γ`: the subgroup of the automorphisms of the binary tree
generated by `a, b, c, d` (Definition 4.6). -/
def GrigorchukGroup : Subgroup BinaryTreeAut :=
  Subgroup.closure {grigA, grigB, grigC, grigD}

namespace GrigorchukGroup

/-- `a` as an element of `Γ`. -/
def a : GrigorchukGroup := ⟨grigA, Subgroup.subset_closure (by simp)⟩
/-- `b` as an element of `Γ`. -/
def b : GrigorchukGroup := ⟨grigB, Subgroup.subset_closure (by simp)⟩
/-- `c` as an element of `Γ`. -/
def c : GrigorchukGroup := ⟨grigC, Subgroup.subset_closure (by simp)⟩
/-- `d` as an element of `Γ`. -/
def d : GrigorchukGroup := ⟨grigD, Subgroup.subset_closure (by simp)⟩

/-- The generating set `S = {a, b, c, d}` of `Γ`. -/
def generators : Set GrigorchukGroup := {a, b, c, d}

end GrigorchukGroup

/-- The `n`-th level stabilizer `St(n)` of `Γ`: the elements fixing every vertex of level `n`,
i.e. every word of length `n`. -/
def levelStabilizer (n : ℕ) : Subgroup GrigorchukGroup where
  carrier := {g | ∀ v : List Bool, v.length = n →
    ((g : BinaryTreeAut) : Equiv.Perm (List Bool)) v = v}
  mul_mem' := by
    intro g h hg hh v hv
    simp only [Subgroup.coe_mul, Equiv.Perm.coe_mul, Function.comp_apply]
    rw [hh v hv, hg v hv]
  one_mem' := by intro v _; rfl
  inv_mem' := by
    intro g hg v hv
    have := hg v hv
    simp only [InvMemClass.coe_inv]
    conv_lhs => rw [← this]
    simp

theorem BinaryTreeAut.append_drop (g : BinaryTreeAut) (v w : List Bool) :
    (g : Equiv.Perm (List Bool)) v ++ ((g : Equiv.Perm (List Bool)) (v ++ w)).drop v.length =
      (g : Equiv.Perm (List Bool)) (v ++ w) := by
  have hp : (g : Equiv.Perm (List Bool)) v <+: (g : Equiv.Perm (List Bool)) (v ++ w) :=
    (g.2.2 v (v ++ w)).1 (List.prefix_append v w)
  have hl := g.2.1 v
  rw [← hl]
  exact List.prefix_iff_eq_append.mp hp


/-- The section `g|_v` of a tree automorphism `g` at a vertex `v`: how `g` acts below `v`,
read as an automorphism of the whole tree. It sends `w` to the word `u` with
`g (v ++ w) = g v ++ u`. For `v = [i]` this is Garrido's `φᵢ(g)`, and `g|_{[i, j, k]}` is
`φₖ(φⱼ(φᵢ(g)))`. -/
def treeSection (g : BinaryTreeAut) (v : List Bool) : BinaryTreeAut :=
  ⟨{ toFun := fun w => ((g : Equiv.Perm (List Bool)) (v ++ w)).drop v.length
     invFun := fun w => (((g⁻¹ : BinaryTreeAut) : Equiv.Perm (List Bool))
        ((g : Equiv.Perm (List Bool)) v ++ w)).drop v.length
     left_inv := by
       intro w
       simp only
       rw [BinaryTreeAut.append_drop g v w]
       simp
     right_inv := by
       intro w
       simp only
       have h1 := BinaryTreeAut.append_drop g⁻¹ ((g : Equiv.Perm (List Bool)) v) w
       have hv : ((g⁻¹ : BinaryTreeAut) : Equiv.Perm (List Bool))
           ((g : Equiv.Perm (List Bool)) v) = v := by simp
       rw [hv, g.2.1 v] at h1
       rw [h1]
       simp only [InvMemClass.coe_inv, Equiv.Perm.mul_apply]
       rw [show (g : Equiv.Perm (List Bool)) ((g : Equiv.Perm (List Bool))⁻¹ ((g : Equiv.Perm (List Bool)) v ++ w)) = (g : Equiv.Perm (List Bool)) v ++ w by simp]
       rw [← g.2.1 v]
       simp },
   by
     refine ⟨fun w => ?_, fun w₁ w₂ => ?_⟩
     · simp only [Equiv.coe_fn_mk, List.length_drop, g.2.1, List.length_append]
       omega
     · simp only [Equiv.coe_fn_mk]
       have e1 := BinaryTreeAut.append_drop g v w₁
       have e2 := BinaryTreeAut.append_drop g v w₂
       calc w₁ <+: w₂ ↔ v ++ w₁ <+: v ++ w₂ := (List.prefix_append_right_inj v).symm
         _ ↔ (g : Equiv.Perm (List Bool)) (v ++ w₁) <+: (g : Equiv.Perm (List Bool)) (v ++ w₂) :=
           g.2.2 _ _
         _ ↔ _ := by rw [e1, e2]
         _ ↔ _ := List.prefix_append_right_inj _⟩

/-- Garrido's notation `u = (u₀, u₁)` for `u ∈ St(1)` (p. 14): the sections of `u` at the two
first-level vertices, `0` then `1`. It is defined on `St(1)` only. -/
def stOnePair (u : levelStabilizer 1) : BinaryTreeAut × BinaryTreeAut :=
  (treeSection ((u : GrigorchukGroup) : BinaryTreeAut) [false],
   treeSection ((u : GrigorchukGroup) : BinaryTreeAut) [true])

/-- The word length `l(g)` of `g ∈ Γ` with respect to `{a, b, c, d}`: the least `n` such that
`g` is a product of at most `n` generators and their inverses. -/
noncomputable def wordLength (g : GrigorchukGroup) : ℕ :=
  sInf {n | g ∈ Chou.wordBall GrigorchukGroup.generators n}

end Garrido

Source

A. Garrido, "An introduction to amenable groups", lecture notes, Oxford Advanced Class in Algebra, Michaelmas 2013 (PDF, Feb 2015), p. 13-14, Definition 4.6 and the notation of Section 4.2; https://web.archive.org/web/20260805000803/https://www.math.uni-duesseldorf.de/~garrido/amenable.pdf

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Read-back: the Grigorchuk group and associated definitions

This item is a bundle of definitions (with a few supporting lemmas that are proved in the file). They share the vocabulary set up in the first two sections.

Words and prefixes

Throughout, a word is a finite sequence $x_1 x_2 \cdots x_k$ of letters from $\{0,1\}$ (the two Boolean values; below, "false" is written $0$ and "true" is written $1$ ). The empty word $\varnothing$ is allowed, and $|v|$ denotes the length of $v$ . Words are read left to right: $x_1$ is the first letter, and concatenation $vw$ means $v$ followed by $w$ . Write $W$ for the set of all words (of every finite length, including $0$ ).

A word $v$ is a prefix of $w$ , written $v \preceq w$ , when there exists a word $t$ with $vt = w$ . (Every word is a prefix of itself, and $\varnothing$ is a prefix of every word.)

Permutations of $W$ are composed as functions: $(\sigma\tau)(v) = \sigma(\tau(v))$ , i.e. $\tau$ is applied first. The identity is the identity map and $\sigma^{-1}$ is the inverse bijection.

1. The group of tree automorphisms, $\mathrm{Aut}(T)$

$\mathrm{Aut}(T)$ is the subgroup of the group of all bijections $W \to W$ consisting of those bijections $\sigma$ such that

$\sigma$ preserves length: $|\sigma(v)| = |v|$ for every word $v$ ; and
$\sigma$ preserves and reflects the prefix relation: for all words $v, w$ ,

v \preceq w \iff \sigma(v) \preceq \sigma(w).

(The file proves this set contains the identity and is closed under composition and inverses.) An element of $\mathrm{Aut}(T)$ is formally such a bijection bundled with the proof of the two properties; it acts on words by applying the underlying bijection. The group operation is composition as above.

2. The four generating maps $a, b, c, d$

Four functions $W \to W$ are defined by recursion on the word:

$a(\varnothing) = \varnothing$ , and $a(x w) = \bar x\, w$ , where $\bar x$ is the other letter. That is, $a$ flips the first letter and leaves the rest unchanged.
$b$ , $c$ , $d$ are defined simultaneously: each fixes $\varnothing$ , and for every word $w$

\begin{aligned} b(0w) &= 0\,a(w), & b(1w) &= 1\,c(w),\\ c(0w) &= 0\,a(w), & c(1w) &= 1\,d(w),\\ d(0w) &= 0\,w, & d(1w) &= 1\,b(w). \end{aligned}

So $b, c, d$ never change the first letter; after a first letter $0$ , $b$ and $c$ apply $a$ to the remainder while $d$ does nothing; after a first letter $1$ , the remainder is acted on by $c$ , $d$ , $b$ respectively. (For example, $b(11010) = 11010$ , $c(11101) = 11100$ , $d(1101) = 1100$ .)

Supporting lemmas proved in the file: each of $a, b, c, d$ is an involution ( $f(f(w)) = w$ for all $w$ ), preserves length, and satisfies $v \preceq w \iff f(v) \preceq f(w)$ for all $v, w$ (with the forward implication also recorded separately for each). Consequently each of $a,b,c,d$ is a bijection of $W$ that is its own inverse, and lies in $\mathrm{Aut}(T)$ . The elements of $\mathrm{Aut}(T)$ so obtained are also called $a, b, c, d$ .

3. The Grigorchuk group $G$

G = \langle a, b, c, d\rangle \le \mathrm{Aut}(T),

the smallest subgroup of $\mathrm{Aut}(T)$ containing the four elements $a,b,c,d$ (the intersection of all subgroups containing them). $G$ is regarded as a group in its own right, whose elements are elements of $\mathrm{Aut}(T)$ lying in this subgroup.

The same four elements, now viewed as elements of $G$ , are again called $a, b, c, d$ , and the generating set of $G$ is the set $S = \{a, b, c, d\} \subseteq G$ .

4. Level stabilizers $\mathrm{St}_G(n)$

For each natural number $n \ge 0$ , $\mathrm{St}_G(n)$ is the subgroup of $G$ (not of $\mathrm{Aut}(T)$ ) consisting of the elements $g \in G$ that fix every word of length exactly $n$ :

\mathrm{St}_G(n) = \{\, g \in G : g(v) = v \text{ for every word } v \text{ with } |v| = n \,\}.

(The file proves this is a subgroup.) Edge case: for $n = 0$ the only word of length $0$ is $\varnothing$ , and every element of $\mathrm{Aut}(T)$ preserves length and so fixes $\varnothing$ ; hence $\mathrm{St}_G(0) = G$ .

A supporting lemma proved in the file: for every $g \in \mathrm{Aut}(T)$ and all words $v, w$ , the word $g(vw)$ equals $g(v)$ followed by the word obtained from $g(vw)$ by deleting its first $|v|$ letters. In other words, $g(vw)$ begins with $g(v)$ .

5. Sections $g|_v$

For $g \in \mathrm{Aut}(T)$ and a word $v$ , the section $g|_v \in \mathrm{Aut}(T)$ is the map

g|_v(w) = \text{the word obtained from } g(vw) \text{ by deleting its first } |v| \text{ letters}.

By the lemma just stated, this is the unique word $u$ with $g(vw) = g(v)\,u$ . Its inverse bijection is $w \mapsto$ (delete the first $|v|$ letters of $g^{-1}(g(v)\,w)$ ). The file proves this is a bijection of $W$ satisfying the two conditions of Section 1, so $g|_v \in \mathrm{Aut}(T)$ . Note that $g|_v$ is defined for every $g \in \mathrm{Aut}(T)$ and every word $v$ (including $v = \varnothing$ , where $g|_\varnothing = g$ as maps) and lands in $\mathrm{Aut}(T)$ , not necessarily in $G$ .

6. The pair of first-level sections

For $u \in \mathrm{St}_G(1)$ (so $u \in G$ fixes both one-letter words $0$ and $1$ ), define

\psi(u) = \bigl(u|_0,\; u|_1\bigr) \in \mathrm{Aut}(T) \times \mathrm{Aut}(T),

the sections of $u$ (as an element of $\mathrm{Aut}(T)$ ) at the words $0$ and $1$ , in that order. This is only a function; nothing in the definition asserts it is a homomorphism, injective, or lands in $G \times G$ .

7. Word length in $G$

For $n \ge 0$ , the ball of radius $n$ with respect to a subset $S$ of a group is the set of all group elements $g$ for which there is a finite list $s_1, \dots, s_k$ of group elements with

$k \le n$ (the empty list, $k=0$ , is allowed and has product the identity),
each $s_i$ satisfies $s_i \in S$ or $s_i^{-1} \in S$ , and
$s_1 s_2 \cdots s_k = g$ (product in list order).

The word length of $g \in G$ is

\ell(g) = \min\{\, n \in \mathbb{N} : g \in B_S(n) \,\},

where $B_S(n)$ is the ball of radius $n$ with respect to the generating set $S = \{a,b,c,d\} \subseteq G$ of Section 3. Junk-value convention: if $g$ lay in no ball $B_S(n)$ , the set would be empty and $\ell(g)$ would be defined to be $0$ . In particular $\ell(1) = 0$ (via the empty list). Since the balls are nested ( $B_S(n) \subseteq B_S(n+1)$ follows from " $k \le n$ "), $\ell(g)$ is the least number of factors from $S \cup S^{-1}$ needed to write $g$ , whenever $g$ can be so written.

Human review

Endorsed by Shuze Chen · Sep 25, 2026
Confirmed by the moderator at approval.
Endorsed by dbenbenn · Sep 25, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

The binary tree, its automorphisms, and the Grigorchuk group

Read-back: the Grigorchuk group and associated definitions

Words and prefixes

1. The group of tree automorphisms, Aut(T)\mathrm{Aut}(T)Aut(T)

2. The four generating maps a,b,c,da, b, c, da,b,c,d

3. The Grigorchuk group GGG

4. Level stabilizers StG(n)\mathrm{St}_G(n)StG​(n)

5. Sections g∣vg|_vg∣v​