Gessel words

AbbreviationGessel alphabet#✓fully proved

For a natural number \(n\), the Gessel alphabet over \(S = [n] = \{1, \dots, n\}\) is the disjoint union of an unbarred copy and a barred copy of \([n]\): it has an unbarred letter \(i\) and a barred letter \(\bar{i}\) for each \(i \in [n]\).

Each copy is indexed by \(\{0, \dots, n - 1\}\), the index \(j\) standing for the label \(j + 1\).

abbrev GesselAlphabet (n : ℕ) : Type :=
  Fin n ⊕ Fin n

Used by 6

Used bySigned balance of a label · Barred occurrences of a label · Unbarred occurrences of a label · Complete Gessel words · Complete Gessel words are the Gessel words of zero balance · Gessel word

DefinitionUnbarred occurrences of a label#✓fully proved

Let \(n\) be a natural number, let \(w\) be a word (a finite sequence of letters) over the Gessel alphabet over \([n] = \{1, \dots, n\}\) and let \(m\) be a natural number. The unbarred count of \(m\) in \(w\) is the number of positions of \(w\) that hold the unbarred letter \(m\); it is \(0\) when \(m \notin [n]\).

def gesselUnbarredCount (n : ℕ) (w : List (GesselAlphabet n)) (m : ℕ) : ℕ :=
  (w.filter fun a => match a with
    | Sum.inl j => decide (j.val + 1 = m)
    | Sum.inr _ => false).length

Uses 1 · Used by 3

Statement usesGessel alphabet

Used bySigned balance of a label · Complete Gessel words · Complete Gessel words are the Gessel words of zero balance

DefinitionBarred occurrences of a label#✓fully proved

Let \(n\) be a natural number, let \(w\) be a word (a finite sequence of letters) over the Gessel alphabet over \([n] = \{1, \dots, n\}\) and let \(m\) be a natural number. The barred count of \(m\) in \(w\) is the number of positions of \(w\) that hold the barred letter \(\bar{m}\); it is \(0\) when \(m \notin [n]\).

def gesselBarredCount (n : ℕ) (w : List (GesselAlphabet n)) (m : ℕ) : ℕ :=
  (w.filter fun a => match a with
    | Sum.inl _ => false
    | Sum.inr j => decide (j.val + 1 = m)).length

Uses 1 · Used by 3

Statement usesGessel alphabet

Used bySigned balance of a label · Complete Gessel words · Complete Gessel words are the Gessel words of zero balance

DefinitionSigned balance of a label#✓fully proved

Let \(n\) be a natural number, let \(w\) be a word over the Gessel alphabet over \([n] = \{1, \dots, n\}\) and let \(m\) be a natural number. The signed balance of \(m\) in \(w\) is the integer obtained by subtracting the number of occurrences of the barred letter \(\bar{m}\) in \(w\) from the number of occurrences of the unbarred letter \(m\) in \(w\); it is \(0\) when \(m \notin [n]\).

def gesselBalance (n : ℕ) (w : List (GesselAlphabet n)) (m : ℕ) : ℤ :=
  (gesselUnbarredCount n w m : ℤ) - (gesselBarredCount n w m : ℤ)

Uses 3 · Used by 2

Statement usesGessel alphabet · Barred occurrences of a label · Unbarred occurrences of a label

Used byComplete Gessel words are the Gessel words of zero balance · Gessel word

DefinitionGessel word#✓fully proved

Let \(n\) be a natural number. For a word \(u\) over the Gessel alphabet over \(S = [n] = \{1, \dots, n\}\) and a natural number \(m\), write \(\beta_u(m)\) for the signed balance of \(m\) in \(u\): the number of occurrences of the unbarred letter \(m\) in \(u\) minus the number of occurrences of the barred letter \(\bar{m}\) in \(u\). A word \(w\) over this alphabet is a Gessel word when, for every prefix \(w'\) of \(w\) (including the empty word and \(w\) itself) and every \(k\) with \(1 \le k \le n\), we have \(\sum_{i=1}^{k} \beta_{w'}(n + 1 - i) \ge 0\), that is, the signed balances in \(w'\) of the \(k\) largest labels \(n, n - 1, \dots, n + 1 - k\) have nonnegative sum.

def IsGesselWord (n : ℕ) (w : List (GesselAlphabet n)) : Prop :=
  ∀ (w' suffix : List (GesselAlphabet n)), w' ++ suffix = w →
    ∀ k : ℕ, 1 ≤ k → k ≤ n →
      0 ≤ ∑ i ∈ Finset.Icc 1 k, gesselBalance n w' (n + 1 - i)

Uses 2 · Used by 2

Statement usesGessel alphabet · Signed balance of a label

Used byComplete Gessel words · Complete Gessel words are the Gessel words of zero balance

DefinitionComplete Gessel words#✓fully proved

A word \(w\) over the Gessel alphabet of \(S = [n] = \{1, \dots, n\}\) is a complete Gessel word when it is a Gessel word and, for every \(m \in [n]\), the unbarred letter \(m\) and the barred letter \(\bar m\) occur the same number of times in \(w\).

def IsCompleteGesselWord (n : ℕ) (w : List (GesselAlphabet n)) : Prop :=
  IsGesselWord n w ∧
    ∀ i : Fin n,
      gesselUnbarredCount n w (i.val + 1) = gesselBarredCount n w (i.val + 1)

Uses 4 · Used by 1

Statement usesGessel alphabet · Gessel word · Barred occurrences of a label · Unbarred occurrences of a label

Used byComplete Gessel words are the Gessel words of zero balance

TheoremComplete Gessel words are the Gessel words of zero balance#✓fully proved

A word \(w\) over the Gessel alphabet of \([n] = \{1, \dots, n\}\) is a complete Gessel word if and only if it is a Gessel word and, for every \(m \in [n]\), the signed balance of \(m\) in \(w\) (the number of occurrences of the unbarred letter \(m\) minus the number of occurrences of the barred letter \(\bar m\)) is zero.

theorem isCompleteGesselWord_iff_balance_eq_zero (n : ℕ) (w : List (GesselAlphabet n)) :
    IsCompleteGesselWord n w ↔
      IsGesselWord n w ∧ ∀ i : Fin n, gesselBalance n w (i.val + 1) = 0

Uses 6

Statement usesGessel alphabet · Complete Gessel words · Gessel word · Signed balance of a label

Proof usesBarred occurrences of a label · Unbarred occurrences of a label

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.