{"version":2,"policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","profile":"std","imports":["Std","Batteries","Lean.Elab.Tactic.Omega"],"statement_hash":"628148448355c1412fae271dced53a7a4b49e9b683daeed6e046f9397beb04e6","problem":{"id":30,"title":"Diff measurement: alignment edit cost equals source plus target length minus twice the keeps","description":"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.\n\nThis 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.","statement":"(fun (source target : List (Sum Nat (Sum Nat Nat)) → List Nat)\n     (cost keeps : List (Sum Nat (Sum Nat Nat)) → Nat) =>\n ∀ script : List (Sum Nat (Sum Nat Nat)),\n cost script + 2 * keeps script = (source script).length + (target script).length)\n(fun script => script.filterMap (fun edit => match edit with\n | .inl x => some x | .inr (.inl x) => some x | .inr (.inr _) => none))\n(fun script => script.filterMap (fun edit => match edit with\n | .inl x => some x | .inr (.inl _) => none | .inr (.inr x) => some x))\n(fun script => script.foldr (fun edit n => match edit with | .inl _ => n | .inr _ => n + 1) 0)\n(fun script => script.foldr (fun edit n => match edit with | .inl _ => n + 1 | .inr _ => n) 0)","profile":"std","module_pins":[],"module_context":[],"scope":{"obligations":["cost_accounting"],"assumptions":["Keep costs zero; insertion and deletion each cost one."],"cost_metric":"edit_count","model_scope":"Keep/delete/insert alignment: cost + twice the keeps equals source length plus target length.","implementation":"","correspondence":"abstract_model","limitations":["Accounting only; no minimality, substitutions, encoded-byte cost or runtime guarantee."]}},"source":null,"proof":null,"proof_url":"/api/v1/submissions/14/proof","source_url":"/api/v1/submissions/14/source","source_hash":"494e8d86b7f07618d7c0613986ce6609a4bd6ceced694451e85c50cf32881bae","proof_bytes":900,"proof_format":"term-trimmed-v1"}