OAI/Combinatorics/LowSpaceSubsetSum/Streams/ModularCursor.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Executable modular row initialization

Binary search finds the first direct pivot and the position after the last complementary pivot. The resulting constant-state cyclic cursor produces the corresponding sorted modular row exactly. The cutoff search uses a supplied number of steps; the theorem requires only that the array length be smaller than 2^k. Equal residues stay separate array occurrences.

  1. def OAI.LowSpaceSubsetSum.ModularCursor.forwardStart line 23
  2. def OAI.LowSpaceSubsetSum.ModularCursor.reverseStart line 28
  3. theorem OAI.LowSpaceSubsetSum.ModularCursor.forward_trace line 33
  4. theorem OAI.LowSpaceSubsetSum.ModularCursor.reverse_trace line 55
  5. theorem OAI.LowSpaceSubsetSum.ModularCursor.forward_sorted line 77
  6. theorem OAI.LowSpaceSubsetSum.ModularCursor.reverse_sorted line 89