# Layer 3 — Text Buffer / Rope (8000 lines target)

## What This Layer Does
The core data structure for editable text: a rope (balanced binary tree of
string chunks) supporting O(log n) insert, delete, and slice. Also owns the
undo tree — a persistent branching history of all edits.

## Repos That Contribute
| Repo | What to pull |
|------|-------------|
| **errant** | QTT tagged memory for rope nodes; Linear Forth ISA pattern for undo stack |
| **sovereign-array** | Lean 4 array language — formal proof of rope invariants; C++20 array ops as rope leaf implementation |

## What to Build First
1. Rope node type — leaf (u8 slice) and branch (left+right child, cached length)
2. Rope concat / split — fundamental O(log n) ops
3. Rope insert / delete — built on concat/split
4. Line index — O(log n) byte-offset to line/col
5. Undo tree — persistent snapshot with branching (not linear stack)
6. Rope invariant proofs — port from sovereign-array Lean 4 proofs

## Key Design Constraints
- Rope nodes allocated from Layer 0 arena; never heap-malloc after init
- Undo tree nodes also in arena; compacted on checkpoint
- QTT tags from errant: each rope leaf carries a provenance tag (for LSP sync)
- Lean 4 proofs from sovereign-array must hold: size(concat(a,b)) = size(a)+size(b)