OAI/Combinatorics/LowSpaceSubsetSum/Storage/PreparedCheckerCells.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Four prepared blocks have polynomial live-buffer overhead

  1. def OAI.LowSpaceSubsetSum.PreparedCheckerCells.scratch line 14
  2. theorem OAI.LowSpaceSubsetSum.PreparedCheckerCells.scratch_bound line 16
  3. theorem OAI.LowSpaceSubsetSum.PreparedCheckerCells.query_left_cells line 27
  4. theorem OAI.LowSpaceSubsetSum.PreparedCheckerCells.query_right_cells line 31
  5. theorem OAI.LowSpaceSubsetSum.PreparedCheckerCells.query_left_value line 35
  6. theorem OAI.LowSpaceSubsetSum.PreparedCheckerCells.query_right_value line 39
  7. theorem OAI.LowSpaceSubsetSum.PreparedCheckerCells.prepared_depths line 43
  8. theorem OAI.LowSpaceSubsetSum.PreparedCheckerCells.numeric line 55
  9. theorem OAI.LowSpaceSubsetSum.PreparedCheckerCells.arrays_cells line 83
  10. theorem OAI.LowSpaceSubsetSum.PreparedCheckerCells.list_payload line 103
  11. def OAI.LowSpaceSubsetSum.PreparedCheckerCells.retained line 114

    Source documentation

    Original entry payloads and their array slots remain shared throughout all filtering, sorting and recursion.

    def retained (left right : Array (StoredEntry n)) : ℕ :=
…

    Mentions: OAI.LowSpaceSubsetSum.StoredEntry

  12. theorem OAI.LowSpaceSubsetSum.PreparedCheckerCells.retained_le line 118
  13. theorem OAI.LowSpaceSubsetSum.PreparedCheckerCells.arrays_with_payload line 126