BinaryMemo.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

A finite binary dictionary for gathered and globally memoized inputs. Each recursive step reads one key bit and touches one node. The explicit counters charge pointer/node operations; multiword key/value processing is accounted for separately by their bit lengths.

theorem OAI.EditApproximation.BinaryMemo.lookup_insert_same line 30
theorem OAI.EditApproximation.BinaryMemo.lookup_insert_other line 36
theorem OAI.EditApproximation.BinaryMemo.lookup_empty line 53
def OAI.EditApproximation.BinaryMemo.nodes line 58
theorem OAI.EditApproximation.BinaryMemo.child_nodes line 62
theorem OAI.EditApproximation.BinaryMemo.insert_nodes line 66
theorem OAI.EditApproximation.BinaryMemo.lookupCosted_spec line 87
Source documentation
An instrumented lookup returns exactly the ordinary dictionary answer, charging one node visit per consumed bit and one terminal visit.
```
theorem lookupCosted_spec (tree : BinaryMemo α) (key : List Bool) :
    tree.lookupCosted key = (tree.lookup key, key.length + 1) := by
…
```
Mentions: OAI.EditApproximation.BinaryMemo
theorem OAI.EditApproximation.BinaryMemo.insertCosted_spec line 97
Source documentation
Persistent insertion allocates one new node at each visited level; the two untouched subtrees are retained by pointer.
```
theorem insertCosted_spec (tree : BinaryMemo α) (key : List Bool) (a : α) :
    tree.insertCosted key a = (tree.insert key a, key.length + 1) := by
…
```
Mentions: OAI.EditApproximation.BinaryMemo
theorem OAI.EditApproximation.binaryMemoKey_length line 109
Source documentation
Fixed-width, least-significant-bit first encoding; no allocation proportional to the numerical magnitude of a key is required.
```
@[simp] theorem binaryMemoKey_length (d n : ℕ) : (binaryMemoKey d n).length = d := by
…
```
Mentions: OAI.EditApproximation.binaryMemoKey
theorem OAI.EditApproximation.binaryMemoKey_injective line 114
theorem OAI.EditApproximation.binaryMemo_lookup_insert line 133