Sequence patches: bounded splice length is original minus deleted plus inserted
Proof verified
typechecked
Pinned formal modules
module #2 · 9537027be7db9dcc4d4eb2eee415ed4e015adcdae5125a7926ef5b3361dda1fc
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.
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.