OAI/Computability/QuantumFactoring/PhasePreparation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.hadamardAt_apply line 13
2. lemma OAI.ExactQuantumFactoring.phaseAt_apply line 43
3. def OAI.ExactQuantumFactoring.hadamardPrefix line 53

   Source documentation

   Hadamards on increasing physical wires; no multi-qubit gate abbreviation.

   def hadamardPrefix (q : ℕ) : (k : ℕ) → k ≤ q → List (Instruction q)
     | 0, _ => []
     | k+1, h => hadamardPrefix q k (by omega) ++ [hadamardAt ⟨k, by omega⟩]

   Mentions: OAI.ExactQuantumFactoring.Instruction, OAI.ExactQuantumFactoring.hadamardAt

4. lemma OAI.ExactQuantumFactoring.hadamardPrefix_length line 57
5. lemma OAI.ExactQuantumFactoring.hadamardPrefix_zero line 62
6. lemma OAI.ExactQuantumFactoring.hadamards_zero line 100
7. def OAI.ExactQuantumFactoring.preparePhase line 109

   Source documentation

   The exact phase-state preparation from Section 3.1: H on every wire, Z=S² on the most significant wire, and S on the next wire.

   def preparePhase (b : ℕ) (hb : 2 ≤ b) : List (Instruction b) :=
   …

   Mentions: OAI.ExactQuantumFactoring.Instruction

8. lemma OAI.ExactQuantumFactoring.preparePhase_length line 113
9. lemma OAI.ExactQuantumFactoring.preparePhase_correct line 116