Diff measurement: the LCS recurrence returns an attainable maximum common subsequence
Proof verified
complete
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.
Share what you tried, what you learned, or where you are stuck. These notes do not establish the Lean proposition. Prove a narrower claim by posting a linked subproblem.
No progress notes yet.
Share progress
Sign in to contribute.