OAI/Combinatorics/LowSpaceSubsetSum/Streams/BinaryPivot.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Bounded binary pivot search

A search state consists of two endpoints of a half-open interval. Each step performs at most one indexed predicate query and halves the interval. The predicate is true on a prefix, including the empty and full prefixes. After k steps with array length less than 2^k, the endpoints agree and identify the exact boundary. This is the pivot rule needed by cyclic modular rows.

  1. structure OAI.LowSpaceSubsetSum.BinaryPivot.Cut line 20
  2. def OAI.LowSpaceSubsetSum.BinaryPivot.initial line 27
  3. def OAI.LowSpaceSubsetSum.BinaryPivot.width line 29
  4. def OAI.LowSpaceSubsetSum.BinaryPivot.step line 31
  5. def OAI.LowSpaceSubsetSum.BinaryPivot.PrefixPredicate line 41
  6. def OAI.LowSpaceSubsetSum.BinaryPivot.Separates line 44
  7. theorem OAI.LowSpaceSubsetSum.BinaryPivot.initial_separates line 47
  8. theorem OAI.LowSpaceSubsetSum.BinaryPivot.step_separates line 56
  9. theorem OAI.LowSpaceSubsetSum.BinaryPivot.step_width_le_half line 75
  10. theorem OAI.LowSpaceSubsetSum.BinaryPivot.iterate_separates line 85
  11. theorem OAI.LowSpaceSubsetSum.BinaryPivot.iterate_width_zero line 93
  12. def OAI.LowSpaceSubsetSum.BinaryPivot.search line 104
  13. theorem OAI.LowSpaceSubsetSum.BinaryPivot.search_exact line 106
  14. theorem OAI.LowSpaceSubsetSum.BinaryPivot.search_split line 123