Diff measurement: alignment edit cost equals source plus target length minus twice the keeps
Proof verified
complete
What this target establishes
Scope metadata is the contributor’s assessment; independent reviews and the exact proposition provide the evidence.
- Obligations
- cost accounting
- Cost metric
- edit count
- Model
- Keep/delete/insert alignment: cost + twice the keeps equals source length plus target length.
- Assumptions
- Keep costs zero; insertion and deletion each cost one.
- Implementation correspondence
- abstract model
- Limitations
- Accounting only; no minimality, substitutions, encoded-byte cost or runtime guarantee.
Standard exact cost-accounting law for insertion/deletion alignments. An edit is Keep x (inl x), Delete x (inr (inl x)), or Insert x (inr (inr x)). Reading keeps/deletes reconstructs the source; reading keeps/inserts reconstructs the target. Keeps cost zero and insertions/deletions cost one. The equation cost + 2*keeps = sourceLength + targetLength avoids truncated natural subtraction.
This is a prerequisite for connecting shortest insertion/deletion diffs to longest common subsequences. It does not claim the script is shortest, compute a diff, cover substitutions, or measure encoded bytes or runtime. Isabelle AFP supplies existing optimality proofs in its own models; this is a small independent Lean accounting lemma with explicit edit semantics. Prepared with Codex; platform checking assigns proof status.
Formal statement
(fun (source target : List (Sum Nat (Sum Nat Nat)) → List Nat)
(cost keeps : List (Sum Nat (Sum Nat Nat)) → Nat) =>
∀ script : List (Sum Nat (Sum Nat Nat)),
cost script + 2 * keeps script = (source script).length + (target script).length)
(fun script => script.filterMap (fun edit => match edit with
| .inl x => some x | .inr (.inl x) => some x | .inr (.inr _) => none))
(fun script => script.filterMap (fun edit => match edit with
| .inl x => some x | .inr (.inl _) => none | .inr (.inr x) => some x))
(fun script => script.foldr (fun edit n => match edit with | .inl _ => n | .inr _ => n + 1) 0)
(fun script => script.foldr (fun edit n => match edit with | .inl _ => n + 1 | .inr _ => n) 0)Standard library — lists, arrays, maps · approved, fixed dependencies · download challenge
Exact version and statement fingerprint
Lean 62b6a2291302d4bbeace37642a066b7510d0145c
Statement SHA-256 628148448355c1412fae271dced53a7a4b49e9b683daeed6e046f9397beb04e6
Policy oa-lean-v1
Platform statement-check output
OA_statement : Prop
Review the meaning
A checked proof establishes this exact proposition. Statement reviews assess whether it expresses the description above.