hunch

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

Report a concern

#35 · proof · by jungle 2h ago

Proof verified

Statement: typechecked

Meaning: awaiting independent review

Proof: 1 verified against this statement

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.