FiniteTreeCosts.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Inexpensive scripts in the recursive row evaluator

Local row advancement and descendant-occurrence lifting establish lem:finite-cost from geometric hypotheses on state translations and invisible leaf decoders.

theorem OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord_eq_orbitRows line 20

theorem OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord_cheap_script line 29

Source documentation

Advancing the rows in one node has exactly the source's deletion/insertion script cost, uniformly in its state (including all ancestor offsets).

theorem nodeWord_cheap_script {m : ℕ} (T : ℕ)
    (leaf : List (Fin m) → A → Γ) (u : List (Fin m) → A)
    (h : ℕ) (p : List (Fin m)) (x : A) (s : ℕ) (hs : s ≤ T) :
    EditScript (nodeWord T leaf u (h + 1) p x)
      (nodeWord T leaf u (h + 1) p (x + s • u p))
      (2 * s * m * (m * T) ^ h) := by
…

Mentions: OAI.TreeEdit.EditScript, OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord

theorem OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord_cheap_editDistance line 40

theorem OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord_descendant_script line 51

Source documentation

A uniform script at one descendant lifts through its T^q.length occurrences. Leaf decoders outside that descendant must be invariant under the same state translation. Every intermediate word remains unrestricted.

theorem nodeWord_descendant_script {m : ℕ} (T : ℕ)
    (leaf : List (Fin m) → A → Γ) (u : List (Fin m) → A)
    (h : ℕ) (q p : List (Fin m)) (z : A) (C : ℕ)
    (hlocal : ∀ y, EditScript (nodeWord T leaf u h (p ++ q) y)
      (nodeWord T leaf u h (p ++ q) (y + z)) C)
    (houtside : ∀ r : List (Fin m), r.length = h + q.length →
      ¬ q.IsPrefix r → ∀ y, leaf (p ++ r) (y + z) = leaf (p ++ r) y)
    (x : A) :
    EditScript (nodeWord T leaf u (h + q.length) p x)
      (nodeWord T leaf u (h + q.length) p (x + z)) (T ^ q.length * C) := by
…

Mentions: OAI.TreeEdit.EditScript, OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord

theorem OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord_leaf_script line 126

Source documentation

Changing only one leaf decoder costs one substitution in each of its T^q.length occurrences, irrespective of how much its state changes.

theorem nodeWord_leaf_script {m : ℕ} (T : ℕ)
    (leaf : List (Fin m) → A → Γ) (u : List (Fin m) → A)
    (q p : List (Fin m)) (z : A)
    (houtside : ∀ r : List (Fin m), r.length = q.length → r ≠ q →
      ∀ y, leaf (p ++ r) (y + z) = leaf (p ++ r) y)
    (x : A) :
    EditScript (nodeWord T leaf u q.length p x)
      (nodeWord T leaf u q.length p (x + z)) (T ^ q.length) := by
…

Mentions: OAI.TreeEdit.EditScript, OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord

theorem OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord_leaf_editDistance line 149

theorem OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord_descendant_cheap_script line 161

Source documentation

Combined local row advancement and occurrence lifting, with exactly the cost T^depth * 2*s*rowLength used in the finite-tree construction.

theorem nodeWord_descendant_cheap_script {m : ℕ} (T : ℕ)
    (leaf : List (Fin m) → A → Γ) (u : List (Fin m) → A)
    (h : ℕ) (q p : List (Fin m)) (s : ℕ) (hs : s ≤ T)
    (houtside : ∀ r : List (Fin m), r.length = h + 1 + q.length →
      ¬ q.IsPrefix r → ∀ y,
        leaf (p ++ r) (y + s • u (p ++ q)) = leaf (p ++ r) y)
    (x : A) :
    EditScript (nodeWord T leaf u (h + 1 + q.length) p x)
      (nodeWord T leaf u (h + 1 + q.length) p (x + s • u (p ++ q)))
      (T ^ q.length * (2 * s * m * (m * T) ^ h)) :=
…

Mentions: OAI.TreeEdit.EditScript, OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord

theorem OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord_descendant_cheap_editDistance line 175

theorem OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord_leaf_normalized_bound line 190

Source documentation

The pointwise leaf-cost estimate in the manuscript's normalized form, with M = (mT)^q.length.

theorem nodeWord_leaf_normalized_bound {m : ℕ} (T : ℕ) (hm : 0 < m)
    (leaf : List (Fin m) → A → Γ) (u : List (Fin m) → A)
    (q p : List (Fin m)) (z : A)
    (houtside : ∀ r : List (Fin m), r.length = q.length → r ≠ q →
      ∀ y, leaf (p ++ r) (y + z) = leaf (p ++ r) y)
    (x : A) :
    (ed (nodeWord T leaf u q.length p x)
      (nodeWord T leaf u q.length p (x + z)) : ℝ) ≤
      ((m * T : ℕ) : ℝ) ^ q.length / (m : ℝ) ^ q.length := by
…

Mentions: OAI.TreeEdit.ed, OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord

theorem OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord_descendant_normalized_bound line 210

Source documentation

Equation eq:finite-cost for the recursive word evaluator: a depth-j translation by s cheap node steps costs at most (2s/T) M/m^j. The decoder-locality hypothesis is exactly what makes other subtrees unchanged.

theorem nodeWord_descendant_normalized_bound {m : ℕ} (T : ℕ)
    (hm : 0 < m) (hT : 0 < T)
    (leaf : List (Fin m) → A → Γ) (u : List (Fin m) → A)
    (h : ℕ) (q p : List (Fin m)) (s : ℕ) (hs : s ≤ T)
    (houtside : ∀ r : List (Fin m), r.length = h + 1 + q.length →
      ¬ q.IsPrefix r → ∀ y,
        leaf (p ++ r) (y + s • u (p ++ q)) = leaf (p ++ r) y)
    (x : A) :
    (ed (nodeWord T leaf u (h + 1 + q.length) p x)
      (nodeWord T leaf u (h + 1 + q.length) p (x + s • u (p ++ q))) : ℝ) ≤
      (2 * (s : ℝ) / T) *
        (((m * T : ℕ) : ℝ) ^ (h + 1 + q.length) / (m : ℝ) ^ q.length) := by
…

Mentions: OAI.TreeEdit.ed, OAI.TreeEdit.BinaryLower.FiniteTree.nodeWord