OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationKeyCells.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Live scratch of the concrete stored-record key

The membership and signed-sum recursions count their live frames. Generated index lists are released between weight calls; masks and input values remain shared. The first projection preserves both the numerical value and work.

  1. def OAI.LowSpaceSubsetSum.RepresentationKeyCells.member line 16
  2. theorem OAI.LowSpaceSubsetSum.RepresentationKeyCells.member_value line 23
  3. theorem OAI.LowSpaceSubsetSum.RepresentationKeyCells.member_cells line 29
  4. def OAI.LowSpaceSubsetSum.RepresentationKeyCells.signedAt line 35
  5. theorem OAI.LowSpaceSubsetSum.RepresentationKeyCells.signedAt_value line 39
  6. theorem OAI.LowSpaceSubsetSum.RepresentationKeyCells.signedAt_cells line 43
  7. def OAI.LowSpaceSubsetSum.RepresentationKeyCells.sumIndices line 50
  8. theorem OAI.LowSpaceSubsetSum.RepresentationKeyCells.sumIndices_value line 60
  9. theorem OAI.LowSpaceSubsetSum.RepresentationKeyCells.sumIndices_cells line 67
  10. def OAI.LowSpaceSubsetSum.RepresentationKeyCells.weight line 78
  11. theorem OAI.LowSpaceSubsetSum.RepresentationKeyCells.weight_value line 82
  12. theorem OAI.LowSpaceSubsetSum.RepresentationKeyCells.weight_cells line 86
  13. def OAI.LowSpaceSubsetSum.RepresentationKeyCells.leafWeight line 93
  14. theorem OAI.LowSpaceSubsetSum.RepresentationKeyCells.leafWeight_value line 100
  15. theorem OAI.LowSpaceSubsetSum.RepresentationKeyCells.leafWeight_cells line 104
  16. def OAI.LowSpaceSubsetSum.RepresentationKeyCells.pairKey line 112
  17. theorem OAI.LowSpaceSubsetSum.RepresentationKeyCells.pairKey_value line 121
  18. theorem OAI.LowSpaceSubsetSum.RepresentationKeyCells.pairKey_cells line 126