OAI/Combinatorics/LowSpaceSubsetSum/Compression/CompressionProgram.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Compression runtime on arbitrary inputs

The runtime data contains only the input. In particular, neither a fixed solution nor evidence of solvability is available to the executable scan. A fixed solution is used only to analyze the success probability of the input-only scan.

  1. structure OAI.LowSpaceSubsetSum.CompressionData line 16
  2. def OAI.LowSpaceSubsetSum.CompressionData.weights line 23
  3. def OAI.LowSpaceSubsetSum.CompressionData.block line 24
  4. def OAI.LowSpaceSubsetSum.CompressionData.leftRaw line 26
  5. def OAI.LowSpaceSubsetSum.CompressionData.rightRaw line 28
  6. def OAI.LowSpaceSubsetSum.CompressionData.storedFirst line 31
  7. def OAI.LowSpaceSubsetSum.CompressionData.storedSecond line 35
  8. def OAI.LowSpaceSubsetSum.CompressionData.groupList line 40
  9. def OAI.LowSpaceSubsetSum.CompressionData.storedRightArray line 43
  10. abbrev OAI.LowSpaceSubsetSum.CompressionData.GroupState line 46
  11. def OAI.LowSpaceSubsetSum.CompressionData.groupStart line 52
  12. def OAI.LowSpaceSubsetSum.CompressionData.groupRead line 57
  13. def OAI.LowSpaceSubsetSum.CompressionData.groupOutput line 65
  14. def OAI.LowSpaceSubsetSum.CompressionData.streamLength line 71
  15. def OAI.LowSpaceSubsetSum.CompressionData.actualLeftDictionary line 74
  16. def OAI.LowSpaceSubsetSum.CompressionData.actualRightHit line 84
  17. def OAI.LowSpaceSubsetSum.CompressionData.compactTests line 94
  18. def OAI.LowSpaceSubsetSum.CompressionData.residuePass line 98
  19. def OAI.LowSpaceSubsetSum.CompressionData.compressionTrial line 105
  20. def OAI.LowSpaceSubsetSum.CompressionData.zeroSetup line 111

    Source documentation

    A zero-target analysis wrapper reuses only group-domain facts. Its empty solution never enters the runtime definitions above.

    def zeroSetup : CompressionSetup n :=
…

    Mentions: OAI.LowSpaceSubsetSum.CompressionSetup

  21. theorem OAI.LowSpaceSubsetSum.CompressionData.groupRead_law line 114
  22. theorem OAI.LowSpaceSubsetSum.CompressionData.groupOutput_mem line 119
  23. theorem OAI.LowSpaceSubsetSum.CompressionData.groupOutput_sorted line 125
  24. theorem OAI.LowSpaceSubsetSum.CompressionData.initial_output_length line 131
  25. def OAI.LowSpaceSubsetSum.CompressionSetup.runtimeData line 142
  26. theorem OAI.LowSpaceSubsetSum.CompressionSetup.runtime_trial_eq line 144