Work.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Finite dependency-path accounting

The double sum is the dependency-path budget in Section 10 of the edit-distance manuscript, with separate branching bounds for same-index and earlier-index requests.

def OAI.EditApproximation.dependencyPathBudget line 19
Source documentation
Overcount of dependency paths with at most depth descending edges and indices strictly earlier-index/pass edges.
```
def dependencyPathBudget (depth indices same earlier : ℕ) : ℕ :=
…
```

theorem OAI.EditApproximation.dependencyPathBudget_le line 25

Source documentation

Explicit bound on the double sum, before substituting asymptotic parameters. All quantities are natural numbers.

theorem dependencyPathBudget_le (depth indices same earlier : ℕ)
    (hsame : 1 ≤ same) (hearlier : 1 ≤ earlier) :
    dependencyPathBudget depth indices same earlier ≤
      (depth + 1) * (indices + 1) * 2 ^ (depth + indices) *
        same ^ depth * earlier ^ indices := by
…

Mentions: OAI.EditApproximation.dependencyPathBudget