Diff measurement: the LCS recurrence returns an attainable maximum common subsequence

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. The 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. Relevant 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.

(fun (lcs : Nat → List Nat → List Nat → Nat) =>
∀ (xs ys : List Nat) (fuel : Nat), xs.length + ys.length ≤ fuel →
 (∃ common : List Nat, common.Sublist xs ∧ common.Sublist ys ∧ common.length = lcs fuel xs ys) ∧
 (∀ common : List Nat, common.Sublist xs → common.Sublist ys → common.length ≤ lcs fuel xs ys))
(fun fuel => Nat.rec (fun _ _ : List Nat => 0)
 (fun _ recur xs ys => match xs, ys with
 | [], _ => 0
 | _, [] => 0
 | x :: xt, y :: yt => if x = y then 1 + recur xt yt
   else max (recur xt ys) (recur xs yt)) fuel)

OA_statement : Prop