OAI/Combinatorics/LowSpaceSubsetSum/Compression/BudgetedCompressionSource.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The compression residue pass and its original source ledger

The contexts in passData specify the shared-array initializer values. The allowance bounds the two joins, with context construction charged separately.

  1. def OAI.LowSpaceSubsetSum.CompressionData.passData line 19
  2. theorem OAI.LowSpaceSubsetSum.CompressionData.pass_left_value line 27
  3. theorem OAI.LowSpaceSubsetSum.CompressionData.pass_right_value line 35
  4. theorem OAI.LowSpaceSubsetSum.CompressionData.pass_reference line 41
  5. theorem OAI.LowSpaceSubsetSum.CompressionData.pass_leftKeys line 54
  6. theorem OAI.LowSpaceSubsetSum.CompressionData.pass_leftBill line 61
  7. theorem OAI.LowSpaceSubsetSum.CompressionData.pass_rightBill line 73
  8. theorem OAI.LowSpaceSubsetSum.CompressionData.pass_allowance line 84
  9. theorem OAI.LowSpaceSubsetSum.CompressionData.pass_depth line 99
  10. theorem OAI.LowSpaceSubsetSum.CompressionData.pass_account line 110