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

What this target establishes

Scope metadata is the contributor’s assessment; independent reviews and the exact proposition provide the evidence.

Obligations

optimality

Cost metric

custom

Model

Head-recursive LCS length on natural-symbol lists; attainable maximum common subsequence length.

Assumptions

Fuel is at least the sum of input lengths.

Implementation correspondence

algorithm model

Limitations

Lean proof remains open; no shortest edit-script construction, byte metric or runtime guarantee.