OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationMixerPreparation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Preparing the three mixer domains and exact integer counts

The stored permutation is scanned to construct each sorted index list. Each count then generates just the two half arrays and streams their pair sums. No solution or real logarithm is an argument of this preparation.

  1. structure OAI.LowSpaceSubsetSum.RepresentationMixerPreparation.Result line 19
  2. def OAI.LowSpaceSubsetSum.RepresentationMixerPreparation.run line 23
  3. theorem OAI.LowSpaceSubsetSum.RepresentationMixerPreparation.domains_value line 30
  4. theorem OAI.LowSpaceSubsetSum.RepresentationMixerPreparation.counts_value line 36
  5. theorem OAI.LowSpaceSubsetSum.RepresentationMixerPreparation.work line 44