StoredEntryTerminal.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Executed terminal weight check on bounded stored entries

The mask list is retained by reference throughout sorting and matching. Only scalar weights are inspected. The ambient size bounds the sort depth, so initialization does not compute a logarithm of a list.

def OAI.LowSpaceSubsetSum.StoredEntryTerminal.lengthAcc line 18
theorem OAI.LowSpaceSubsetSum.StoredEntryTerminal.lengthAcc_eq line 22

def OAI.LowSpaceSubsetSum.StoredEntryTerminal.findAcc line 29

Source documentation

Tail-recursive matching with each scalar subtraction and comparison charged.

def findAcc (target : ℤ) : ℕ → List (StoredEntry n) → List (StoredEntry n) → ℕ → Bool × ℕ
  | 0, _, _, work => (false, work + 1)
  | _ + 1, [], _, work => (false, work + 2)
  | _ + 1, _ :: _, [], work => (false, work + 3)
  | fuel + 1, x :: xs, y :: ys, work =>
    let a := x.value
…

Mentions: OAI.LowSpaceSubsetSum.StoredEntry

theorem OAI.LowSpaceSubsetSum.StoredEntryTerminal.findAcc_value line 40
theorem OAI.LowSpaceSubsetSum.StoredEntryTerminal.findAcc_work line 61
def OAI.LowSpaceSubsetSum.StoredEntryTerminal.leftCompare line 79
def OAI.LowSpaceSubsetSum.StoredEntryTerminal.rightCompare line 81
def OAI.LowSpaceSubsetSum.StoredEntryTerminal.run line 85
Source documentation
The two lengths are computed once and reused as the matching limit.
```
def run (target : ℤ) (xs ys : List (StoredEntry n)) : Bool × ℕ :=
…
```
Mentions: OAI.LowSpaceSubsetSum.StoredEntry
theorem OAI.LowSpaceSubsetSum.StoredEntryTerminal.left_value line 94
theorem OAI.LowSpaceSubsetSum.StoredEntryTerminal.right_value line 100
theorem OAI.LowSpaceSubsetSum.StoredEntryTerminal.run_value line 108
theorem OAI.LowSpaceSubsetSum.StoredEntryTerminal.run_work line 117
theorem OAI.LowSpaceSubsetSum.StoredEntryTerminal.bounded_value line 136
Source documentation
This bounded terminal agrees with the separator depth-first search.
```
theorem bounded_value (target : ℤ) (xs ys : List (StoredEntry n))
    (h : xs.length + ys.length ≤ 2 ^ n) :
    (run target xs ys).1 =
      (SeparatorTerminal.bounded n StoredEntry.value StoredEntry.value target xs ys).accepted := by
…
```
Mentions: OAI.LowSpaceSubsetSum.StoredEntry, OAI.LowSpaceSubsetSum.StoredEntryTerminal.run, OAI.LowSpaceSubsetSum.SeparatorTerminal.bounded
theorem OAI.LowSpaceSubsetSum.StoredEntryTerminal.correct line 143
theorem OAI.LowSpaceSubsetSum.StoredEntryTerminal.semantic_value line 151
Source documentation
Erasure to the original finite-set record is only a proof view.
```
theorem semantic_value (target : ℤ) (xs ys : List (StoredEntry n))
    (hx : xs.length ≤ 2 ^ n) (hy : ys.length ≤ 2 ^ n) :
    (run target xs ys).1 =
      (SeparatorTerminal.run Entry.value Entry.value target
        (xs.map StoredEntry.semantic) (ys.map StoredEntry.semantic)).accepted := by
…
```
Mentions: OAI.LowSpaceSubsetSum.StoredEntry, OAI.LowSpaceSubsetSum.StoredEntryTerminal.run, OAI.LowSpaceSubsetSum.SeparatorTerminal.run, OAI.LowSpaceSubsetSum.StoredEntry.semantic
theorem OAI.LowSpaceSubsetSum.StoredEntryTerminal.run_expanded line 161
Source documentation
The matching limit is the sum of the two counted lengths.
```
theorem run_expanded (target : ℤ) (xs ys : List (StoredEntry n)) :
    run target xs ys =
      if xs.isEmpty || ys.isEmpty then
        (false, (2 * xs.length + 1) + (2 * ys.length + 1) + 3)
      else
        let left := MeasuredSort.run leftCompare n xs
…
```
Mentions: OAI.LowSpaceSubsetSum.StoredEntry, OAI.LowSpaceSubsetSum.StoredEntryTerminal.run, OAI.LowSpaceSubsetSum.MeasuredSort.run, OAI.LowSpaceSubsetSum.StoredEntryTerminal.leftCompare