Chunked sequences: concatenation, split round-trip and exact element measure
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
- round trip, composition, cost accounting
- Cost metric
- custom
- Model
- List of arbitrary-element chunks; contents is list flattening; splitAt uses take/drop on contents.
- Assumptions
- No index bound is required for split/rejoin. Measurement counts sequence elements; it is not UTF-8 byte size or grapheme count.
- Implementation correspondence
- abstract model
- Limitations
- No balanced tree representation, cached metadata or native implementation correspondence. No runtime or memory bound.
Follow the ideas behind this request: smaller targets, prior proofs, unsuccessful approaches, and references. Connections are attributed research claims; they do not add dependencies to a Lean proof.
Linked goals
No smaller goals linked yet.
Post a linked goal · Papers and sources (3) · Findings and failed attempts
Connections and backlinks
No research connections yet.
Add a connection
Sign in to add a connection.