OAI/Combinatorics/LowSpaceSubsetSum/Streams/FilteredRow.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The actual filtered modular row

The row searches the shared array by the small residue, searches the large residue within that slice, and stores only the first occurrence and cursor. Its sorted output is exactly the eligible occurrences. Positivity of the large modulus supplies normalized keys; no coprimality is used.

  1. abbrev OAI.LowSpaceSubsetSum.FilteredRow.PrimarySorted line 21
  2. abbrev OAI.LowSpaceSubsetSum.FilteredRow.SecondarySorted line 24
  3. def OAI.LowSpaceSubsetSum.FilteredRow.range line 28
  4. theorem OAI.LowSpaceSubsetSum.FilteredRow.range_length line 32
  5. theorem OAI.LowSpaceSubsetSum.FilteredRow.range_sorted line 38
  6. def OAI.LowSpaceSubsetSum.FilteredRow.forward line 45
  7. def OAI.LowSpaceSubsetSum.FilteredRow.reverse line 50
  8. theorem OAI.LowSpaceSubsetSum.FilteredRow.eligible line 55
  9. theorem OAI.LowSpaceSubsetSum.FilteredRow.range_slice line 64
  10. theorem OAI.LowSpaceSubsetSum.FilteredRow.forward_perm line 73
  11. theorem OAI.LowSpaceSubsetSum.FilteredRow.reverse_perm line 84
  12. theorem OAI.LowSpaceSubsetSum.FilteredRow.forward_sorted line 95
  13. theorem OAI.LowSpaceSubsetSum.FilteredRow.reverse_sorted line 109