OAI/Computability/QuantumFactoring/PhysicalListNetworks.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.PhysicalListSlots.sampleNet line 22
  2. lemma OAI.ExactQuantumFactoring.PhysicalListSlots.sampleNet_eval line 24
  3. def OAI.ExactQuantumFactoring.PhysicalListSlots.ordinaryNet line 26
  4. lemma OAI.ExactQuantumFactoring.PhysicalListSlots.ordinaryNet_eval line 28
  5. lemma OAI.ExactQuantumFactoring.PhysicalListSlots.ordinaryNet_count line 34
  6. def OAI.ExactQuantumFactoring.PhysicalListSlots.outputNet line 42
  7. lemma OAI.ExactQuantumFactoring.PhysicalListSlots.outputNet_eval line 44
  8. lemma OAI.ExactQuantumFactoring.PhysicalListSlots.outputNet_count line 50
  9. def OAI.ExactQuantumFactoring.PhysicalListSlots.singleZeroNet line 59

    Source documentation

    Copy the runtime modulus into each literal sampler block; all other input cells are zero. Only fixed wire placements and constants are used.

    def singleZeroNet (n : ℕ) : BooleanNetwork n (ListSampler.width n) :=
…

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.ListSampler.width

  10. lemma OAI.ExactQuantumFactoring.PhysicalListSlots.singleZeroNet_eval line 61
  11. lemma OAI.ExactQuantumFactoring.PhysicalListSlots.singleZeroNet_count line 72
  12. def OAI.ExactQuantumFactoring.PhysicalListSlots.ordinaryZeroNet line 80
  13. lemma OAI.ExactQuantumFactoring.PhysicalListSlots.ordinaryZeroNet_eval line 82
  14. lemma OAI.ExactQuantumFactoring.PhysicalListSlots.ordinaryZeroNet_count line 87
  15. def OAI.ExactQuantumFactoring.PhysicalListSlots.initialNet line 90
  16. lemma OAI.ExactQuantumFactoring.PhysicalListSlots.initialNet_eval line 92
  17. lemma OAI.ExactQuantumFactoring.PhysicalListSlots.initialNet_count line 95
  18. abbrev OAI.ExactQuantumFactoring.PhysicalListSlots.work line 101
  19. abbrev OAI.ExactQuantumFactoring.PhysicalListSlots.launchWidth line 102
  20. def OAI.ExactQuantumFactoring.PhysicalListSlots.launch line 104

    Source documentation

    Length-uniform placement of the completed runtime-modulus list sampler.

    def launch (n : ℕ) : List (Instruction (launchWidth n)) :=
…

    Mentions: OAI.ExactQuantumFactoring.Instruction, OAI.ExactQuantumFactoring.PhysicalListSlots.launchWidth

  21. lemma OAI.ExactQuantumFactoring.PhysicalListSlots.launch_state line 106
  22. lemma OAI.ExactQuantumFactoring.PhysicalListSlots.launch_length line 111