OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationArrayInitialization.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Initialization retaining explicit shared arrays

The row closure captures the shared right array. Row and reader callbacks reuse this array without rebuilding it.

  1. theorem OAI.LowSpaceSubsetSum.RepresentationArrayInitialization.key_apply line 15
  2. def OAI.LowSpaceSubsetSum.RepresentationArrayInitialization.tree line 22
  3. theorem OAI.LowSpaceSubsetSum.RepresentationArrayInitialization.tree_value line 29
  4. def OAI.LowSpaceSubsetSum.RepresentationArrayInitialization.start line 40
  5. theorem OAI.LowSpaceSubsetSum.RepresentationArrayInitialization.start_value line 55
  6. theorem OAI.LowSpaceSubsetSum.RepresentationArrayInitialization.start_work line 73