OAI/Computability/QuantumFactoring/PreparedOracle.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.targetRegister line 19
2. lemma OAI.ExactQuantumFactoring.targetRegister_val line 28
3. lemma OAI.ExactQuantumFactoring.packed_targetRegister line 31
4. lemma OAI.ExactQuantumFactoring.packed_replace_target line 36
5. def OAI.ExactQuantumFactoring.targetProgram line 62
6. lemma OAI.ExactQuantumFactoring.targetProgram_basis line 65
7. def OAI.ExactQuantumFactoring.preparedOracle line 76

   Source documentation

   Prepare a runtime-dependent input with a genuine clean Boolean oracle, then run the same fixed quantum program on that fresh input. All old bits x survive, and c is a network, not a large table of counterfactual outputs.

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

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

8. lemma OAI.ExactQuantumFactoring.preparedOracle_length line 80
9. lemma OAI.ExactQuantumFactoring.preparedOracle_basis line 87
10. lemma OAI.ExactQuantumFactoring.preparedOracle_state line 97

    Source documentation

    Coherent launch on an arbitrary already-entangled classical history. This identity is valid on the actual amplitudes, prior to any later validation.

    lemma preparedOracle_state {n m r : ℕ} (c : BooleanNetwork n m) (hr : c.net.count ≤ r)
        (ops : List (Instruction m)) (ψ : State n) :
        (programMatrix (preparedOracle c hr ops)).mulVec
          (encodeState (fun x => packed r x (fun _ => false)) ψ)=
        encodeState (fun xy : Basis n×Basis m => packed r xy.1 xy.2)
          (RecordedHistory.appendState ψ (fun x => (programMatrix ops).mulVec (basisVector (c.eval x)))) := by
    …

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.Instruction, OAI.ExactQuantumFactoring.State, OAI.ExactQuantumFactoring.programMatrix, OAI.ExactQuantumFactoring.preparedOracle, OAI.ExactQuantumFactoring.encodeState, OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.RecordedHistory.appendState, OAI.ExactQuantumFactoring.basisVector

11. lemma OAI.ExactQuantumFactoring.packed_pair_injective line 114