OAI/Combinatorics/LowSpaceSubsetSum/Storage/MixerOrderExecution.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Three comparisons for the stable mixer order

Only strict count inversions are exchanged. Equal counts retain the original index order, exactly as in the lexicographic mathematical sorting convention.

  1. def OAI.LowSpaceSubsetSum.MixerOrderExecution.sort line 13
  2. theorem OAI.LowSpaceSubsetSum.MixerOrderExecution.sort_value line 25
  3. def OAI.LowSpaceSubsetSum.MixerOrderExecution.run line 33
  4. theorem OAI.LowSpaceSubsetSum.MixerOrderExecution.run_value line 36
  5. theorem OAI.LowSpaceSubsetSum.MixerOrderExecution.run_work line 40