OAI/Combinatorics/EditApproximation/Probability/Exact.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

An executable exact cut recurrence

This is the exact source-cut dynamic programming recurrence on ordinary lists and natural numbers. The proof identifies its value with unrestricted unit-cost edit distance. Storage and evaluation costs are separate from this value-level recurrence.

  1. def OAI.EditApproximation.finiteNatMinimum line 19
  2. theorem OAI.EditApproximation.le_finiteNatMinimum_iff line 23
  3. theorem OAI.EditApproximation.finiteNatMinimum_le_member line 32
  4. def OAI.EditApproximation.exactCutCost line 41
  5. theorem OAI.EditApproximation.edit_nil_left line 47
  6. theorem OAI.EditApproximation.exactCutCost_eq_edit line 54