TieBuffer.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

A bounded tie-group buffer

The tail-recursive collector stores at most the requested number of matching occurrences and leaves the first different-key occurrence unconsumed. Its instrumented query counter counts every reader call, including the final lookahead. No clearing of unused buffer positions is performed.

def OAI.LowSpaceSubsetSum.TieBuffer.groupView line 21
structure OAI.LowSpaceSubsetSum.TieBuffer.Result line 24
def OAI.LowSpaceSubsetSum.TieBuffer.fillAcc line 29
def OAI.LowSpaceSubsetSum.TieBuffer.fill line 37
theorem OAI.LowSpaceSubsetSum.TieBuffer.fillAcc_spec line 40
theorem OAI.LowSpaceSubsetSum.TieBuffer.fill_buffer line 78
theorem OAI.LowSpaceSubsetSum.TieBuffer.fill_size_le line 83
theorem OAI.LowSpaceSubsetSum.TieBuffer.fill_suffix line 90
theorem OAI.LowSpaceSubsetSum.TieBuffer.fill_queries_le line 96
theorem OAI.LowSpaceSubsetSum.TieBuffer.fillAcc_queries_le_potential line 103
Source documentation
The collector reads each stored occurrence once and performs at most one additional lookahead, irrespective of the chosen buffer capacity.
```
theorem fillAcc_queries_le_potential (read : σ → Option (α × σ)) (key : α → ℤ) (K : ℤ)
    (view : σ → List α) (hread : RowMerge.IsReader read view)
    (fuel : ℕ) (s : σ) (buf : Array α) (q : ℕ) :
    (fillAcc read key K fuel s buf q).queries ≤
      q + min fuel ((groupView key K view s).length + 1) := by
…
```
Mentions: OAI.LowSpaceSubsetSum.RowMerge.IsReader, OAI.LowSpaceSubsetSum.TieBuffer.fillAcc, OAI.LowSpaceSubsetSum.TieBuffer.groupView
theorem OAI.LowSpaceSubsetSum.TieBuffer.fill_queries_le_potential line 128
def OAI.LowSpaceSubsetSum.TieBuffer.hasKey line 135
theorem OAI.LowSpaceSubsetSum.TieBuffer.hasKey_iff line 140
theorem OAI.LowSpaceSubsetSum.TieBuffer.long_group_full_buffer line 155
Source documentation
A snapshot is needed only if more than B second-row occurrences have this key. In particular the buffer is full when a snapshot is taken.
```
theorem long_group_full_buffer (read : σ → Option (α × σ)) (key : α → ℤ) (K : ℤ)
    (view : σ → List α) (hread : RowMerge.IsReader read view) (B : ℕ) (s : σ)
    (hlong : hasKey read key K (fill read key K B s).cursor = true) :
    B < (groupView key K view s).length ∧ (fill read key K B s).buffer.size = B := by
…
```
Mentions: OAI.LowSpaceSubsetSum.RowMerge.IsReader, OAI.LowSpaceSubsetSum.TieBuffer.hasKey, OAI.LowSpaceSubsetSum.TieBuffer.fill, OAI.LowSpaceSubsetSum.TieBuffer.groupView