FiniteTreeInstantiation.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

Instantiate the recursive word evaluator with the explicit finite state group and subtree vectors.

def OAI.TreeEdit.BinaryLower.FiniteTree.extendPrefix line 16
Source documentation
Total extension of a node prefix to a full leaf path. Its unused tail is irrelevant to every vector at the depth of that prefix.
```
def extendPrefix {m k : ℕ} (i₀ : Fin m) (p : List (Fin m)) : Fin k → Fin m :=
…
```
theorem OAI.TreeEdit.BinaryLower.FiniteTree.agrees_extendPrefix_iff line 19
theorem OAI.TreeEdit.BinaryLower.FiniteTree.extendPrefix_leaf line 37
theorem OAI.TreeEdit.BinaryLower.FiniteTree.extendPrefix_append line 43
def OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriods line 62
Source documentation
The actual leaf periods, in the list-path presentation used by the words.
```
def wordPeriods {m k : ℕ} (primes : Fin k → Fin m → ℕ) : Leaf m k → ℕ :=
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.Leaf
def OAI.TreeEdit.BinaryLower.FiniteTree.wordU line 66
Source documentation
Actual cheap subgroup vector at a list prefix.
```
def wordU {m k : ℕ} (primes : Fin k → Fin m → ℕ) (i₀ : Fin m)
    (p : List (Fin m)) : State (wordPeriods primes) :=
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.State, OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriods
def OAI.TreeEdit.BinaryLower.FiniteTree.wordW line 72
Source documentation
Actual distinguished subgroup vector at a list prefix.
```
def wordW {m k : ℕ} (primes : Fin k → Fin m → ℕ) (i₀ : Fin m)
    (p : List (Fin m)) : State (wordPeriods primes) :=
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.State, OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriods

def OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriod line 78

Source documentation

Prescribed period at a list prefix.

def wordPeriod {m k : ℕ} (primes : Fin k → Fin m → ℕ) (i₀ : Fin m)
    (p : List (Fin m)) : ℕ :=
…

def OAI.TreeEdit.BinaryLower.FiniteTree.finiteWord line 83
Source documentation
The concrete tree word at an arbitrary node.
```
def finiteWord {m k : ℕ} (primes : Fin k → Fin m → ℕ) (i₀ : Fin m)
    (T h : ℕ) (p : List (Fin m)) (x : State (wordPeriods primes)) :
    List (Symbol (wordPeriods primes)) :=
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.State, OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriods, OAI.TreeEdit.BinaryLower.FiniteTree.Symbol
theorem OAI.TreeEdit.BinaryLower.FiniteTree.finiteWord_length line 89
theorem OAI.TreeEdit.BinaryLower.FiniteTree.ofFn_leafEquiv line 94
theorem OAI.TreeEdit.BinaryLower.FiniteTree.wordU_on_child line 102
Source documentation
Concrete vector restriction to a child in the list-path presentation.
```
theorem wordU_on_child {m k : ℕ} (primes : Fin k → Fin m → ℕ)
    (i₀ i : Fin m) (p : List (Fin m)) (hp : p.length < k)
    (l : Leaf m k) (hl : p ++ [i] <+: l.val) :
    wordU primes i₀ p l = wordW primes i₀ (p ++ [i]) l := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.Leaf, OAI.TreeEdit.BinaryLower.FiniteTree.wordU, OAI.TreeEdit.BinaryLower.FiniteTree.wordW
theorem OAI.TreeEdit.BinaryLower.FiniteTree.wordW_on_child line 118
Source documentation
Distinguished parent shift restricts to the current level product times the distinguished child shift.
```
theorem wordW_on_child {m k : ℕ} (primes : Fin k → Fin m → ℕ)
    (i₀ i : Fin m) (p : List (Fin m)) (hp : p.length < k)
    (l : Leaf m k) (hl : p ++ [i] <+: l.val) :
    wordW primes i₀ p l =
      (FiniteVectors.levelProduct primes ⟨p.length, hp⟩ : ℤ) •
        wordW primes i₀ (p ++ [i]) l := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.Leaf, OAI.TreeEdit.BinaryLower.FiniteTree.wordW, OAI.TreeEdit.BinaryLower.FiniteVectors.levelProduct
theorem OAI.TreeEdit.BinaryLower.FiniteTree.wordW_leaf_self line 131
theorem OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriod_leaf line 139
theorem OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriod_nsmul_wordW line 146
Source documentation
The exact prescribed period annihilates the actual word's node vector.
```
theorem wordPeriod_nsmul_wordW {m k : ℕ} (primes : Fin k → Fin m → ℕ)
    (i₀ : Fin m) (p : List (Fin m)) :
    wordPeriod primes i₀ p • wordW primes i₀ p = 0 := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriod, OAI.TreeEdit.BinaryLower.FiniteTree.wordW
theorem OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriod_root line 153
theorem OAI.TreeEdit.BinaryLower.FiniteTree.wordU_off_subtree line 156
theorem OAI.TreeEdit.BinaryLower.FiniteTree.wordW_off_subtree line 164
theorem OAI.TreeEdit.BinaryLower.FiniteTree.finiteWord_leaf_deficit line 173
Source documentation
Base case of the separation proposition for the concrete word construction.
```
theorem finiteWord_leaf_deficit {m k : ℕ} (primes : Fin k → Fin m → ℕ)
    (i₀ : Fin m) (T : ℕ) (p : List (Fin m)) (hp : p.length = k)
    (x : State (wordPeriods primes)) (t : ℤ)
    (ht : ¬ (wordPeriod primes i₀ p : ℤ) ∣ t) :
    deficit 1 (finiteWord primes i₀ T 0 p x)
      (finiteWord primes i₀ T 0 p (x + t • wordW primes i₀ p)) = 1 := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.State, OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriods, OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriod, OAI.TreeEdit.BinaryLower.deficit, OAI.TreeEdit.BinaryLower.FiniteTree.finiteWord, OAI.TreeEdit.BinaryLower.FiniteTree.wordW

theorem OAI.TreeEdit.BinaryLower.FiniteTree.finiteWord_child_relative line 185

Source documentation

The actual relative child translation in any two rows of a node.

theorem finiteWord_child_relative {m k : ℕ} (primes : Fin k → Fin m → ℕ)
    (i₀ i : Fin m) (T h : ℕ) (p : List (Fin m))
    (hlen : p.length + (h + 1) = k) (x : State (wordPeriods primes))
    (t : ℤ) (a b : ℕ) :
    finiteWord primes i₀ T h (p ++ [i])
        (x + t • wordW primes i₀ p + b • wordU primes i₀ p) =
      finiteWord primes i₀ T h (p ++ [i])
        (x + a • wordU primes i₀ p +
          ((b : ℤ) - (a : ℤ) + t *
            (FiniteVectors.levelProduct primes ⟨p.length, by omega⟩ : ℤ)) •
              wordW primes i₀ (p ++ [i])) := by
…

Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.State, OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriods, OAI.TreeEdit.BinaryLower.FiniteTree.finiteWord, OAI.TreeEdit.BinaryLower.FiniteTree.wordW, OAI.TreeEdit.BinaryLower.FiniteTree.wordU, OAI.TreeEdit.BinaryLower.FiniteVectors.levelProduct

theorem OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriods_pos line 205
Source documentation
Positive prime entries make every cyclic leaf period positive.
```
theorem wordPeriods_pos {m k : ℕ} (primes : Fin k → Fin m → ℕ)
    (hpos : ∀ j i, 0 < primes j i) (l : Leaf m k) : 0 < wordPeriods primes l := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.Leaf, OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriods
theorem OAI.TreeEdit.BinaryLower.FiniteTree.finite_wordState line 211
Source documentation
The concrete parameter group is finite, not merely a formal product.
```
theorem finite_wordState {m k : ℕ} (primes : Fin k → Fin m → ℕ)
    (hpos : ∀ j i, 0 < primes j i) : Finite (State (wordPeriods primes)) := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.State, OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriods
theorem OAI.TreeEdit.BinaryLower.FiniteTree.finite_wordSymbol line 218
Source documentation
The actual tagged cyclic-state alphabet is finite.
```
theorem finite_wordSymbol {m k : ℕ} (primes : Fin k → Fin m → ℕ)
    (hpos : ∀ j i, 0 < primes j i) : Finite (Symbol (wordPeriods primes)) := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.Symbol, OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriods
def OAI.TreeEdit.BinaryLower.FiniteTree.rootWord line 225
Source documentation
Root words, retaining their exact common length in the type.
```
def rootWord {m k : ℕ} (primes : Fin k → Fin m → ℕ) (i₀ : Fin m) (T : ℕ)
    (x : State (wordPeriods primes)) : Word (Symbol (wordPeriods primes)) ((m * T) ^ k) :=
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.State, OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriods, OAI.TreeEdit.Word, OAI.TreeEdit.BinaryLower.FiniteTree.Symbol