OAI/Computability/QuantumFactoring/PhaseOracle.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.phase_twice_basis line 21
2. def OAI.ExactQuantumFactoring.BooleanNetwork.phaseTarget line 36
3. def OAI.ExactQuantumFactoring.BooleanNetwork.phaseOracle line 40

   Source documentation

   Predicate phase kickback is a clean oracle, two S gates, and the same clean XOR oracle again, all over the fixed gate alphabet.

   def phaseOracle {n r : ℕ} (c : BooleanNetwork n 1) (hr : c.net.count ≤ r) :
       List (Instruction (n+1+r)) :=
   …

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

4. lemma OAI.ExactQuantumFactoring.BooleanNetwork.phaseOracle_length line 44
5. lemma OAI.ExactQuantumFactoring.BooleanNetwork.phaseOracle_basis line 50
6. lemma OAI.ExactQuantumFactoring.BooleanNetwork.phaseOracle_state line 67

   Source documentation

   The same actual program applies its diagonal predicate phase coherently, not just on classical basis inputs.

   lemma phaseOracle_state {n r : ℕ} (c : BooleanNetwork n 1) (hr : c.net.count ≤ r)
       (ψ : Basis n → ℂ) :
       (programMatrix (phaseOracle c hr)).mulVec
         (encodeState (fun x => packed r x (fun _ : Fin 1 => false)) ψ) =
         encodeState (fun x => packed r x (fun _ : Fin 1 => false))
           (fun x => (if c.eval x 0 then (-1:ℂ) else 1)*ψ x) := by
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.programMatrix, OAI.ExactQuantumFactoring.BooleanNetwork.phaseOracle, OAI.ExactQuantumFactoring.encodeState, OAI.ExactQuantumFactoring.BooleanNetwork.packed

7. def OAI.ExactQuantumFactoring.BooleanNetwork.allZero line 83

   Source documentation

   Bounded fan-in conjunction, built incrementally, not an unbounded gate.

   def allZero (n : ℕ) : (k : ℕ) → k ≤ n → BooleanNetwork n 1
     | 0, _ => constant true
     | k+1, h => (allZero n k (by omega)).band (bit ⟨k,by omega⟩).bnot

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.BooleanNetwork.constant, OAI.ExactQuantumFactoring.BooleanNetwork.band, OAI.ExactQuantumFactoring.BooleanNetwork.bit, OAI.ExactQuantumFactoring.BooleanNetwork.bnot

8. lemma OAI.ExactQuantumFactoring.BooleanNetwork.allZero_count line 87
9. lemma OAI.ExactQuantumFactoring.BooleanNetwork.allZero_eval line 93
10. lemma OAI.ExactQuantumFactoring.BooleanNetwork.allZero_full line 109