{"version":1,"policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","profile":"core","imports":["Init"],"statement_hash":"c101ee7711ebbf72758815011dc5eb7d383d5109c75f11cd646bf5fc4f72bc92","problem":{"id":29,"title":"Diff measurement: the LCS recurrence returns an attainable maximum common subsequence","description":"Porting target for an established machine-checked result, not a new conjecture. Isabelle AFP Longest_Common_Subsequence proves lcs_correct: its recurrence equals the maximum common-subsequence length. This self-contained Lean target restates the core obligation using head recursion, natural-number symbols and an explicit fuel bound.\n\nThe first conclusion requires a common subsequence attaining the computed length. The second says none is longer. List.Sublist preserves order and permits gaps. Fuel at least the sum of input lengths prevents truncation. The source uses an indexed recurrence; universal equivalence to its executable implementation is not assumed or claimed.\n\nRelevant to insertion/deletion diff optimality, but this target does not yet prove the shortest-edit-script formula, substitution-based Levenshtein distance, a Myers implementation, memoization or a runtime bound. The existing Isabelle proof is supplied as an attributed source; a Lean proof of this exact target remains requested. Prepared with Codex.","statement":"(fun (lcs : Nat → List Nat → List Nat → Nat) =>\n∀ (xs ys : List Nat) (fuel : Nat), xs.length + ys.length ≤ fuel →\n (∃ common : List Nat, common.Sublist xs ∧ common.Sublist ys ∧ common.length = lcs fuel xs ys) ∧\n (∀ common : List Nat, common.Sublist xs → common.Sublist ys → common.length ≤ lcs fuel xs ys))\n(fun fuel => Nat.rec (fun _ _ : List Nat => 0)\n (fun _ recur xs ys => match xs, ys with\n | [], _ => 0\n | _, [] => 0\n | x :: xt, y :: yt => if x = y then 1 + recur xt yt\n   else max (recur xt ys) (recur xs yt)) fuel)","profile":"core","module_pins":[],"module_context":[],"scope":{"obligations":["optimality"],"assumptions":["Fuel is at least the sum of input lengths."],"cost_metric":"custom","model_scope":"Head-recursive LCS length on natural-symbol lists; attainable maximum common subsequence length.","implementation":"","correspondence":"algorithm_model","limitations":["Lean proof remains open; no shortest edit-script construction, byte metric or runtime guarantee."]}},"source":"import Init\n\ndef OA_statement : Prop := ((fun (lcs : Nat → List Nat → List Nat → Nat) =>\n∀ (xs ys : List Nat) (fuel : Nat), xs.length + ys.length ≤ fuel →\n (∃ common : List Nat, common.Sublist xs ∧ common.Sublist ys ∧ common.length = lcs fuel xs ys) ∧\n (∀ common : List Nat, common.Sublist xs → common.Sublist ys → common.length ≤ lcs fuel xs ys))\n(fun fuel => Nat.rec (fun _ _ : List Nat => 0)\n (fun _ recur xs ys => match xs, ys with\n | [], _ => 0\n | _, [] => 0\n | x :: xt, y :: yt => if x = y then 1 + recur xt yt\n   else max (recur xt ys) (recur xs yt)) fuel))\n\n#check OA_statement\n","proof":null}