OAI/Computability/QuantumFactoring/BooleanCircuit.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.basisVector line 13
  2. lemma OAI.ExactQuantumFactoring.matrix_basisVector line 16
  3. lemma OAI.ExactQuantumFactoring.permutationMatrix_basisVector line 21
  4. def OAI.ExactQuantumFactoring.Instruction.liftPerm line 29

    Source documentation

    Lift a local classical reversible gate to the actual wires; this is not an additional circuit instruction, just its classical semantics.

    noncomputable def Instruction.liftPerm {q : ℕ} (o : Instruction q)
    (e : Equiv.Perm (Basis o.gate.arity)) : Equiv.Perm (Basis q) :=
…

    Mentions: OAI.ExactQuantumFactoring.Instruction, OAI.ExactQuantumFactoring.Basis

  5. lemma OAI.ExactQuantumFactoring.Instruction.liftPerm_matrix line 33
  6. lemma OAI.ExactQuantumFactoring.Instruction.liftPerm_wire line 51
  7. lemma OAI.ExactQuantumFactoring.Instruction.liftPerm_unused line 58
  8. lemma OAI.ExactQuantumFactoring.Instruction.liftPerm_basisVector line 65
  9. abbrev OAI.ExactQuantumFactoring.plainGate line 72

    Source documentation

    No inverse/control flag is used in these elementary fresh-bit operations.

    abbrev plainGate (p : Primitive) : Gate := ⟨p,false,false⟩

    Mentions: OAI.ExactQuantumFactoring.Primitive, OAI.ExactQuantumFactoring.Gate

  10. lemma OAI.ExactQuantumFactoring.plainGate_arity line 74
  11. lemma OAI.ExactQuantumFactoring.plainGate_localMatrix line 77
  12. abbrev OAI.ExactQuantumFactoring.notAt line 80
  13. abbrev OAI.ExactQuantumFactoring.cnotAt line 86
  14. abbrev OAI.ExactQuantumFactoring.toffoliAt line 92
  15. lemma OAI.ExactQuantumFactoring.notAt_lift line 99
  16. lemma OAI.ExactQuantumFactoring.cnotAt_lift line 110
  17. lemma OAI.ExactQuantumFactoring.toffoliAt_lift line 127
  18. lemma OAI.ExactQuantumFactoring.notAt_basis line 149
  19. lemma OAI.ExactQuantumFactoring.cnotAt_basis line 153
  20. lemma OAI.ExactQuantumFactoring.toffoliAt_basis line 158