BitMemoHeap.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A cumulative allocation counter for the actual memo execution. It keeps all local allocations until the entire run finishes, so it also bounds peak space. A read retains three continuation/result cells. Each memo call reserves its address workspace, key bits, traversal frames and the possible new trie path; existing values and input words are shared by reference.

def OAI.EditApproximation.BitQuery.Heap.runCells line 17
theorem OAI.EditApproximation.BitQuery.Heap.runCells_le line 27
def OAI.EditApproximation.rankedBitMemoCells line 56
Source documentation
Sixteen scalar/frame slots suffice in addition to eight slots per key bit and the supplied address-construction workspace; the larger fixed reserve also covers the result record and the empty-trie case.
```
def rankedBitMemoCells {κ : Type*} (rank : κ → ℕ)
    (program : (key : κ) → BitQuery {child : κ // rank child < rank key} BinaryFraction)
    (heap : ∀ key, BitQuery.Heap (program key))
    (bits : ℕ) (encode addressCells : κ → ℕ) (key : κ) (memory : BinaryMemo BinaryFraction) : ℕ :=
…
```
Mentions: OAI.EditApproximation.BitQuery, OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.BitQuery.Heap, OAI.EditApproximation.BinaryMemo
theorem OAI.EditApproximation.rankedBitMemoCells_le line 70