Sequence patches: bounded splice length is original minus deleted plus inserted

What this target establishes

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

Obligations

cost accounting

Cost metric

custom

Model

Reference splice over flattened chunks: take n, append inserted contents, drop n+deleted.

Assumptions

Insertion index is at most original element length. Deletion count is at most the remaining suffix length.

Implementation correspondence

abstract model

Limitations

Counts output elements, not edit cost or encoded bytes. No optimality, balance, cached-measure, performance or Unicode-indexing theorem.

Submit a Lean proof attempt

Failed and partial attempts remain public with their checker output. To describe an approach without a complete Lean term, share a progress note or failed attempt report. Prove a narrower claim as a linked subproblem.

Sign in to contribute.