OAI/Combinatorics/LowSpaceSubsetSum/Storage/SumReaderCells.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Live storage of the ordinary sum tournament and distinct counter

The two arrays are immutable and shared. Tournament nodes include bounded path representations, and the counter retains only its current tree. The stream of Cartesian pairs is never materialized.

  1. def OAI.LowSpaceSubsetSum.SumReaderCells.key line 16
  2. def OAI.LowSpaceSubsetSum.SumReaderCells.read line 18
  3. def OAI.LowSpaceSubsetSum.SumReaderCells.width line 22
  4. def OAI.LowSpaceSubsetSum.SumReaderCells.front line 24
  5. theorem OAI.LowSpaceSubsetSum.SumReaderCells.front_value line 33
  6. theorem OAI.LowSpaceSubsetSum.SumReaderCells.front_cells line 38
  7. def OAI.LowSpaceSubsetSum.SumReaderCells.tree line 45
  8. theorem OAI.LowSpaceSubsetSum.SumReaderCells.tree_value line 49
  9. def OAI.LowSpaceSubsetSum.SumReaderCells.start line 56
  10. theorem OAI.LowSpaceSubsetSum.SumReaderCells.start_value line 64
  11. def OAI.LowSpaceSubsetSum.SumReaderCells.next line 77
  12. theorem OAI.LowSpaceSubsetSum.SumReaderCells.next_value line 82
  13. def OAI.LowSpaceSubsetSum.SumReaderCells.stateCells line 88
  14. theorem OAI.LowSpaceSubsetSum.SumReaderCells.stateCells_eq line 91
  15. theorem OAI.LowSpaceSubsetSum.SumReaderCells.next_cells line 95
  16. def OAI.LowSpaceSubsetSum.SumReaderCells.count line 103
  17. theorem OAI.LowSpaceSubsetSum.SumReaderCells.count_value line 109
  18. theorem OAI.LowSpaceSubsetSum.SumReaderCells.count_cells_raw line 114
  19. theorem OAI.LowSpaceSubsetSum.SumReaderCells.scalar_bound line 133
  20. theorem OAI.LowSpaceSubsetSum.SumReaderCells.padded_pow line 149
  21. theorem OAI.LowSpaceSubsetSum.SumReaderCells.normalize_count_bound line 154
  22. theorem OAI.LowSpaceSubsetSum.SumReaderCells.count_bound_of_raw line 157
  23. theorem OAI.LowSpaceSubsetSum.SumReaderCells.count_cells line 173