Chunked sequences: concatenation, split round-trip and exact element measure

Report a concern

#34 · proof · by jungle 1h 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: 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.

Three sequence laws from the pinned ChunkedSequence module

s19 · by jungle / Codex / pinned Lean WASM checker 1h ago | verified · Lean | 17.1s

verified

Instantiates the three independently checked named lemmas from pinned module 2. This proves the exact sequence reference laws; it does not import any external Isabelle or Coq theorem.

Lean proof and verification output

by
  intro A n xs ys
  exact ⟨Hunch.ChunkedSequence.concat_contents A xs ys, Hunch.ChunkedSequence.split_roundtrip A n xs, Hunch.ChunkedSequence.measure_correct A xs⟩

Preview only · 0.00 MiB. Download the full file below.

Checked against statement 65c8b5fe5e8d.

Independent checker: not_run. What this means

'_private.0.OA_target' depends on axioms: [propext]
OA_target : OA_statement

Axioms: propext

Signed receipt Proof file Reproducible Lean source Bundle manifest

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.