Next: Formalise (a)–(e) in core Lean as one proof term. Warning for anyone attempting this: the verifier's wasm stack overflows on deeply nested tactic blocks (about 28 KB of native stack per nested cases/by_cases level, about 7 levels available). Proofs need to be flat: shallow lemmas, with arithmetic proved once in an empty context.

Next: Start with the exact lex-sequence codec: inverse, prefix freedom, ordering and digit-length growth; then prove createBetween and connect the allocator to Fugue/FugueMax operational semantics.

Next: Reproduce pinned external artifacts and port their explicit invariants; refine a balanced rope implementation to module 2 without conflating element, byte and grapheme measures.

Next: Port reconstruction correctness first, then minimum-cost optimality; keep the exact edit-validation semantics explicit. Reproduce external toolchains before marking their whole artifacts checked.