OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionInitializationCells.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Compression tournament construction with live storage

The already-built left and right arrays are retained by the caller. The initializer reads them by index and creates only the padded tournament; there is no row-array copy for an individual tournament leaf.

  1. def OAI.LowSpaceSubsetSum.CompressionInitializationCells.front line 18
  2. theorem OAI.LowSpaceSubsetSum.CompressionInitializationCells.front_value line 31
  3. theorem OAI.LowSpaceSubsetSum.CompressionInitializationCells.front_cells line 39
  4. def OAI.LowSpaceSubsetSum.CompressionInitializationCells.tree line 54
  5. theorem OAI.LowSpaceSubsetSum.CompressionInitializationCells.tree_value line 59
  6. theorem OAI.LowSpaceSubsetSum.CompressionInitializationCells.padded_pow line 73
  7. theorem OAI.LowSpaceSubsetSum.CompressionInitializationCells.tree_cells line 78
  8. def OAI.LowSpaceSubsetSum.CompressionInitializationCells.start line 110
  9. theorem OAI.LowSpaceSubsetSum.CompressionInitializationCells.start_value line 123
  10. theorem OAI.LowSpaceSubsetSum.CompressionInitializationCells.start_cells line 133