FiniteTreeCostTheorem.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The finite tree’s pointwise translation estimates

The concrete finiteWord and cyclic-state vectors satisfy lem:finite-cost. Coordinate support follows from the vector definitions.

theorem OAI.TreeEdit.BinaryLower.FiniteTree.wordU_off_prefix line 15
theorem OAI.TreeEdit.BinaryLower.FiniteTree.wordW_off_prefix line 25
theorem OAI.TreeEdit.BinaryLower.FiniteTree.wordW_leaf_other line 35
theorem OAI.TreeEdit.BinaryLower.FiniteTree.finiteWord_leaf_translation_script line 48
Source documentation
The exact T^k-cost script for arbitrary integer changes to a single cyclic leaf coordinate. The distinguished vector at a leaf is its unit vector.
```
theorem finiteWord_leaf_translation_script {m k : ℕ}
    (primes : Fin k → Fin m → ℕ) (i₀ : Fin m) (T : ℕ)
    (ell : Leaf m k) (t : ℤ) (x : State (wordPeriods primes)) :
    EditScript (finiteWord primes i₀ T k [] x)
      (finiteWord primes i₀ T k [] (x + t • wordW primes i₀ ell.val)) (T ^ k) := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.Leaf, OAI.TreeEdit.BinaryLower.FiniteTree.State, OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriods, OAI.TreeEdit.EditScript, OAI.TreeEdit.BinaryLower.FiniteTree.finiteWord, OAI.TreeEdit.BinaryLower.FiniteTree.wordW
theorem OAI.TreeEdit.BinaryLower.FiniteTree.finiteWord_leaf_translation_cost line 60
Source documentation
First assertion of lem:finite-cost: every state and every integer multiple of a leaf unit vector has edit cost at most M/m^k.
```
theorem finiteWord_leaf_translation_cost {m k : ℕ}
    (primes : Fin k → Fin m → ℕ) (i₀ : Fin m) (T : ℕ)
    (ell : Leaf m k) (t : ℤ) (x : State (wordPeriods primes)) :
    (ed (finiteWord primes i₀ T k [] x)
      (finiteWord primes i₀ T k [] (x + t • wordW primes i₀ ell.val)) : ℝ) ≤
      ((m * T : ℕ) : ℝ) ^ k / (m : ℝ) ^ k := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.Leaf, OAI.TreeEdit.BinaryLower.FiniteTree.State, OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriods, OAI.TreeEdit.ed, OAI.TreeEdit.BinaryLower.FiniteTree.finiteWord, OAI.TreeEdit.BinaryLower.FiniteTree.wordW

theorem OAI.TreeEdit.BinaryLower.FiniteTree.finiteWord_node_translation_script line 73

Source documentation

An ordinary edit script advances the rows at every occurrence of a node.

theorem finiteWord_node_translation_script {m k : ℕ}
    (primes : Fin k → Fin m → ℕ) (i₀ : Fin m) (T : ℕ)
    (q : List (Fin m)) (hq : q.length < k)
    (s : ℕ) (hs : s ≤ T) (x : State (wordPeriods primes)) :
    EditScript (finiteWord primes i₀ T k [] x)
      (finiteWord primes i₀ T k [] (x + s • wordU primes i₀ q))
      (T ^ q.length * (2 * s * m * (m * T) ^ (k - (q.length + 1)))) := by
…

Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.State, OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriods, OAI.TreeEdit.EditScript, OAI.TreeEdit.BinaryLower.FiniteTree.finiteWord, OAI.TreeEdit.BinaryLower.FiniteTree.wordU

theorem OAI.TreeEdit.BinaryLower.FiniteTree.finiteWord_node_translation_cost line 88
Source documentation
Equation eq:finite-cost with the concrete root word, actual cheap vector, and exact source constants. It holds uniformly at every state and also includes the harmless zero shift.
```
theorem finiteWord_node_translation_cost {m k : ℕ}
    (primes : Fin k → Fin m → ℕ) (i₀ : Fin m) (T : ℕ) (hT : 0 < T)
    (q : List (Fin m)) (hq : q.length < k)
    (s : ℕ) (hs : s ≤ T) (x : State (wordPeriods primes)) :
    (ed (finiteWord primes i₀ T k [] x)
      (finiteWord primes i₀ T k [] (x + s • wordU primes i₀ q)) : ℝ) ≤
      (2 * (s : ℝ) / T) * (((m * T : ℕ) : ℝ) ^ k / (m : ℝ) ^ q.length) := by
…
```
Mentions: OAI.TreeEdit.BinaryLower.FiniteTree.State, OAI.TreeEdit.BinaryLower.FiniteTree.wordPeriods, OAI.TreeEdit.ed, OAI.TreeEdit.BinaryLower.FiniteTree.finiteWord, OAI.TreeEdit.BinaryLower.FiniteTree.wordU