ExactSuffixDPWork.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

A costed implementation of the exact cut dynamic program. The counter counts symbol comparisons and list-cell visits, with explicit outer-loop overhead. Each counted transition uses a fixed number of word operations; the surrounding RAM realization supplies that constant. Suffix lookups and occurrence scans are charged rather than treated as constant-time arrays.

theorem OAI.EditApproximation.dpLength_spec line 25
theorem OAI.EditApproximation.dpDrop_spec line 32
theorem OAI.EditApproximation.dpTake_spec line 43
theorem OAI.EditApproximation.dpGetD_spec line 55
theorem OAI.EditApproximation.dpMember_spec line 66
theorem OAI.EditApproximation.dpSingleton_spec line 79
theorem OAI.EditApproximation.dpMinimum_spec line 93
theorem OAI.EditApproximation.dpCandidate_value line 103
theorem OAI.EditApproximation.dpCandidate_work line 110
theorem OAI.EditApproximation.nat_pair_sum_bound line 126
theorem OAI.EditApproximation.dpCell_value line 139
theorem OAI.EditApproximation.dpCell_work line 148
theorem OAI.EditApproximation.chargedSuffixDP_value line 170
theorem OAI.EditApproximation.chargedSuffixDP_work line 177

theorem OAI.EditApproximation.chargedSuffixDP_storage line 205

Source documentation

Every retained row has linear length, and every stored distance fits the input length bound; the traversal counter is polynomial even with lists.

theorem chargedSuffixDP_storage {α : Type*} [DecidableEq α] (source target : List α)
    (N : ℕ) (hsize : source.length + target.length ≤ N) :
    (chargedSuffixDP source target).1.length ≤ N + 1 ∧
      (∀ j ≤ target.length, (chargedSuffixDP source target).1.getD j 0 ≤ N) ∧
      (chargedSuffixDP source target).2 ≤ 50 * (N + 1) ^ 4 := by
…

Mentions: OAI.EditApproximation.chargedSuffixDP

theorem OAI.EditApproximation.dpTake_allocation line 226
theorem OAI.EditApproximation.dpCandidate_allocation line 237
theorem OAI.EditApproximation.nat_list_sum_mono line 244
theorem OAI.EditApproximation.dpCell_allocation line 258
Source documentation
Candidate pairs, natural candidate values, the index range and prefix lists are counted as materialized cells. The fallback prefix is retained.
```
theorem dpCell_allocation {α : Type*} [DecidableEq α] (a : α) (target : List α)
    (previous : List ℕ) (j : ℕ) : dpCellAllocation target j ≤ (dpCell a target previous j).2 := by
…
```
Mentions: OAI.EditApproximation.dpCellAllocation, OAI.EditApproximation.dpCell
theorem OAI.EditApproximation.suffixDPAllocation_le_work line 273
Source documentation
Total materialized list cells over the whole run. This also bounds the simultaneously live materialized cells under any deallocation policy.
```
theorem suffixDPAllocation_le_work {α : Type*} [DecidableEq α] (source target : List α) :
    suffixDPAllocation source target ≤ (chargedSuffixDP source target).2 := by
…
```
Mentions: OAI.EditApproximation.suffixDPAllocation, OAI.EditApproximation.chargedSuffixDP
theorem OAI.EditApproximation.suffixDPAllocation_polynomial line 291