StoredSeparatorQueries.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

Stored-mask codes and executed separator interval queries

A coordinate row is an explicit vector of ambient indices. Every mask bit is obtained by scanning the bounded stored index list. Its binary code then indexes an already prepared incidence table. Two measured binary searches answer the interval query without scanning that incidence list.

def OAI.LowSpaceSubsetSum.StoredSeparatorQueries.code line 21
Source documentation
The callback is executed once for every coordinate.
```
def code : (g : ℕ) → (Fin g → Bool × ℕ) → ℕ × ℕ
  | 0, _ => (0, 1)
  | g + 1, bits =>
    let first := bits 0
…
```
theorem OAI.LowSpaceSubsetSum.StoredSeparatorQueries.code_value line 28
theorem OAI.LowSpaceSubsetSum.StoredSeparatorQueries.code_work line 37
def OAI.LowSpaceSubsetSum.StoredSeparatorQueries.localMask line 48
def OAI.LowSpaceSubsetSum.StoredSeparatorQueries.localCode line 51
theorem OAI.LowSpaceSubsetSum.StoredSeparatorQueries.localCode_value line 58
theorem OAI.LowSpaceSubsetSum.StoredSeparatorQueries.localCode_work line 67
theorem OAI.LowSpaceSubsetSum.StoredSeparatorQueries.localMask_coordinates line 74
def OAI.LowSpaceSubsetSum.StoredSeparatorQueries.lookup line 82
Source documentation
One indexed read after computing a bounded mask's local code.
```
def lookup (row : Vector (Fin n) g) (x : StoredEntry n)
    (store : Array (Array ℕ)) (hs : store.size = 2 ^ g) : Array ℕ × ℕ :=
…
```
Mentions: OAI.LowSpaceSubsetSum.StoredEntry
theorem OAI.LowSpaceSubsetSum.StoredSeparatorQueries.lookup_value line 87
theorem OAI.LowSpaceSubsetSum.StoredSeparatorQueries.lookup_work line 93
theorem OAI.LowSpaceSubsetSum.StoredSeparatorQueries.contains_value line 98
theorem OAI.LowSpaceSubsetSum.StoredSeparatorQueries.avoids_value line 105
theorem OAI.LowSpaceSubsetSum.StoredSeparatorQueries.search_unique line 113
def OAI.LowSpaceSubsetSum.StoredSeparatorQueries.lower line 132
Source documentation
The caller supplies a cached number of binary-search steps.
```
def lower (steps : ℕ) (a : Array ℕ) (r : ℕ) : ℕ × ℕ :=
…
```
theorem OAI.LowSpaceSubsetSum.StoredSeparatorQueries.lower_value line 136
theorem OAI.LowSpaceSubsetSum.StoredSeparatorQueries.lower_work line 149
def OAI.LowSpaceSubsetSum.StoredSeparatorQueries.hit line 153
theorem OAI.LowSpaceSubsetSum.StoredSeparatorQueries.hit_value line 158
theorem OAI.LowSpaceSubsetSum.StoredSeparatorQueries.hit_work line 163