OAI/Computability/QuantumFactoring/CleanPermutation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.BooleanNetwork.packed_single_swap line 12
2. def OAI.ExactQuantumFactoring.BooleanNetwork.swapPrefix line 40
3. lemma OAI.ExactQuantumFactoring.BooleanNetwork.swapPrefix_length line 45
4. lemma OAI.ExactQuantumFactoring.BooleanNetwork.swapPrefix_basis line 51
5. lemma OAI.ExactQuantumFactoring.BooleanNetwork.swapBlocks_basis line 71
6. def OAI.ExactQuantumFactoring.BooleanNetwork.cleanPermutation line 80

   Source documentation

   The standard clean implementation of a bijection uses a verified forward and inverse Boolean network, two work registers, and only the named gates.

   def cleanPermutation {n r : ℕ} (f g : BooleanNetwork n n)
       (hf : f.net.count ≤ r) (hg : g.net.count ≤ r) : List (Instruction (n+n+r)) :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.Instruction

7. lemma OAI.ExactQuantumFactoring.BooleanNetwork.cleanPermutation_basis line 84
8. lemma OAI.ExactQuantumFactoring.BooleanNetwork.cleanPermutation_length line 96