OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationPrimePreparation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Drawing the nested primes after materializing the accepted prefix

The sampler is called with the stored integer widths. Coupling histories occur in erased type transports and correspondence proofs only.

  1. structure OAI.LowSpaceSubsetSum.RepresentationPrimePreparation.Data line 17
  2. theorem OAI.LowSpaceSubsetSum.RepresentationPrimePreparation.widths_ideal line 22
  3. def OAI.LowSpaceSubsetSum.RepresentationPrimePreparation.run line 36
  4. theorem OAI.LowSpaceSubsetSum.RepresentationPrimePreparation.work line 50
  5. theorem OAI.LowSpaceSubsetSum.RepresentationPrimePreparation.complete line 66
  6. theorem OAI.LowSpaceSubsetSum.RepresentationPrimePreparation.source line 109
  7. theorem OAI.LowSpaceSubsetSum.RepresentationPrimePreparation.moduli_ideal line 147
  8. theorem OAI.LowSpaceSubsetSum.RepresentationPrimePreparation.moduli_pos line 159