OAI/Computability/QuantumFactoring/RegisterBasis.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.Register.replace line 13

    Source documentation

    Replace just one placed register, keeping every other physical wire.

    noncomputable def Register.replace {p q : ℕ} (w : Register p q) (x : Basis q) (y : Basis p) : Basis q :=
…

    Mentions: OAI.ExactQuantumFactoring.Register, OAI.ExactQuantumFactoring.Basis

  2. lemma OAI.ExactQuantumFactoring.Register.replace_inside line 16
  3. lemma OAI.ExactQuantumFactoring.Register.replace_outside line 21
  4. lemma OAI.ExactQuantumFactoring.Register.pairState_basis line 26
  5. lemma OAI.ExactQuantumFactoring.Register.pairState_replace_basis line 38
  6. lemma OAI.ExactQuantumFactoring.placed_basis line 46
  7. def OAI.ExactQuantumFactoring.swapAt line 55

    Source documentation

    SWAP is three named CNOT gates, not an extra primitive.

    def swapAt {q : ℕ} (a b : Fin q) (h : a ≠ b) : List (Instruction q) :=
…

    Mentions: OAI.ExactQuantumFactoring.Instruction

  8. lemma OAI.ExactQuantumFactoring.swapAt_basis line 58