OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationStoredPreparationCells.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Full prepared prefix storage, including leaf and coordinate arrays

The accepted prefix remains live through leaf allocation and coordinate sorting. The branch order and all returned work counters are preserved.

  1. def OAI.LowSpaceSubsetSum.RepresentationStoredPreparationCells.extend line 19
  2. def OAI.LowSpaceSubsetSum.RepresentationStoredPreparationCells.run line 34
  3. theorem OAI.LowSpaceSubsetSum.RepresentationStoredPreparationCells.value line 44
  4. theorem OAI.LowSpaceSubsetSum.RepresentationStoredPreparationCells.extend_cells line 67
  5. theorem OAI.LowSpaceSubsetSum.RepresentationStoredPreparationCells.scalar_bound line 83
  6. theorem OAI.LowSpaceSubsetSum.RepresentationStoredPreparationCells.cells line 104