OAI/Computability/QuantumFactoring/PhysicalSplit.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ExactQuantumFactoring.FixedSplit.ordersWidth line 22
  2. def OAI.ExactQuantumFactoring.FixedSplit.ordersLayout line 23
  3. def OAI.ExactQuantumFactoring.FixedSplit.ordersProgram line 25
  4. lemma OAI.ExactQuantumFactoring.FixedSplit.ordersProgram_state line 27
  5. def OAI.ExactQuantumFactoring.FixedSplit.listWires line 40
  6. def OAI.ExactQuantumFactoring.FixedSplit.modulusWires line 42
  7. def OAI.ExactQuantumFactoring.FixedSplit.listEncoding line 44
  8. lemma OAI.ExactQuantumFactoring.FixedSplit.listWires_eval line 46
  9. lemma OAI.ExactQuantumFactoring.FixedSplit.modulusWires_eval line 49
  10. def OAI.ExactQuantumFactoring.FixedSplit.baseNet line 52
  11. lemma OAI.ExactQuantumFactoring.FixedSplit.baseNet_eval line 55
  12. lemma OAI.ExactQuantumFactoring.FixedSplit.baseNet_count line 59
  13. def OAI.ExactQuantumFactoring.FixedSplit.orderInitialNet line 63
  14. lemma OAI.ExactQuantumFactoring.FixedSplit.orderInitialNet_eval line 66
  15. lemma OAI.ExactQuantumFactoring.FixedSplit.orderInitialNet_count line 69
  16. def OAI.ExactQuantumFactoring.FixedSplit.ordersInitialNet line 73
  17. lemma OAI.ExactQuantumFactoring.FixedSplit.ordersInitialNet_eval line 75
  18. lemma OAI.ExactQuantumFactoring.FixedSplit.ordersInitialNet_count line 80
  19. abbrev OAI.ExactQuantumFactoring.FixedSplit.work line 85
  20. abbrev OAI.ExactQuantumFactoring.FixedSplit.width line 86
  21. def OAI.ExactQuantumFactoring.FixedSplit.program line 89

    Source documentation

    One actual fixed-gate circuit: the completed random list is generated first; only that same list supplies the bases for the ensuing order slots.

    def program (n : ℕ) : List (Instruction (width n)) :=
…

    Mentions: OAI.ExactQuantumFactoring.Instruction, OAI.ExactQuantumFactoring.FixedSplit.width

  22. def OAI.ExactQuantumFactoring.FixedSplit.encoding line 91
  23. def OAI.ExactQuantumFactoring.FixedSplit.zero line 93
  24. theorem OAI.ExactQuantumFactoring.FixedSplit.program_state line 96
  25. lemma OAI.ExactQuantumFactoring.FixedSplit.encoding_injective line 105
  26. lemma OAI.ExactQuantumFactoring.FixedSplit.program_length line 116